let B be B_Lattice; :: thesis: for a, b being Element of holds
( a [= b iff a "/\" (b ` ) = Bottom B )
let a, b be Element of ; :: thesis: ( a [= b iff a "/\" (b ` ) = Bottom B )
reconsider B' = B as 0_Lattice ;
reconsider B'' = B as 1_Lattice ;
reconsider D = B as D_Lattice ;
reconsider a' = a, b' = b, c' = a "/\" (b ` ) as Element of ;
reconsider a'' = a, b'' = b as Element of ;
reconsider a1 = a, b1 = b as Element of ;
thus ( a [= b implies a "/\" (b ` ) = Bottom B ) :: thesis: ( a "/\" (b ` ) = Bottom B implies a [= b )

proof

assume a [= b ; :: thesis: a "/\" (b ` ) = Bottom B
then a = a "/\" b by LATTICES:21;
hence a "/\" (b ` ) = a "/\" (b "/\" (b ` )) by LATTICES:def 7
.= a' "/\" (Bottom B') by LATTICES:47
.= Bottom B by LATTICES:40 ;
:: thesis: verum

end;

assume a "/\" (b ` ) = Bottom B ; :: thesis: a [= b
then b = b' "\/" c' by LATTICES:39
.= (b1 "\/" a1) "/\" (b1 "\/" (b1 ` )) by LATTICES:31
.= (b'' "\/" a'') "/\" (Top B'') by LATTICES:48
.= a "\/" b by LATTICES:43 ;
hence a [= b by LATTICES:def 3; :: thesis: verum