bottomeqd Show Code edit
thm (bottomeqd () (
hyp1 (-> ph (z.= A B)))
(-> ph (z.= (bottom A) (bottom B)))
hyp1 A B bottomeq syl
(-> ph (z.= (bottom A) (bottom B)))
)
edit