eqid Show Code edit
## Reflexive Property
thm (eqid () () (= A A)
A A df-eq
(<-> (= A A) (/\ (z.= (z.* (top A) (bottom A)) (z.* (top A) (bottom A))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom A) (z.0)))))
(z.* (top A) (bottom A)) z.eqid
(z.= (z.* (top A) (bottom A)) (z.* (top A) (bottom A)))
(z.= (bottom A) (z.0)) biid
(<-> (z.= (bottom A) (z.0)) (z.= (bottom A) (z.0)))
pm3.2i
(/\ (z.= (z.* (top A) (bottom A)) (z.* (top A) (bottom A))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom A) (z.0))))
mpbirRemove
(= A A)
)
edit