Goal: (K⊥↔⊥)
System: S5(m)
using derived rules: true
1. S5(m) ⊢ (⊥→K⊥)	(A1)
2. S5(m) ⊢ (K⊥→⊥)	(A3)
3. S5(m) ⊢ (K⊥↔⊥)	(EI:1,2)