let B be B_Lattice; :: thesis: for a, b being Element of B holds
( a [= b iff a "/\" (b `) = Bottom B )
let a, b be Element of B; :: thesis: ( a [= b iff a "/\" (b `) = Bottom B )
reconsider B9 = B as 0_Lattice ;
reconsider B99 = B as 1_Lattice ;
reconsider D = B as D_Lattice ;
reconsider a9 = a, b9 = b, c9 = a "/\" (b `) as Element of B9 ;
reconsider a99 = a, b99 = b as Element of B99 ;
reconsider a1 = a, b1 = b as Element of D ;
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:4;
hence a "/\" (b `) = a "/\" (b "/\" (b `)) by LATTICES:def 7
.= a9 "/\" (Bottom B9) by LATTICES:20
.= Bottom B ;
:: thesis: verum

end;

assume a "/\" (b `) = Bottom B ; :: thesis: a [= b
then b = b9 "\/" c9
.= (b1 "\/" a1) "/\" (b1 "\/" (b1 `)) by LATTICES:11
.= (b99 "\/" a99) "/\" (Top B99) by LATTICES:21
.= a "\/" b ;
hence a [= b ; :: thesis: verum