let L be B_Lattice; :: thesis: for a, b being Element of L holds
( b "/\" a = Bottom L iff b [= a ` )
let a, b be Element of L; :: thesis: ( b "/\" a = Bottom L iff b [= a ` )
thus ( b "/\" a = Bottom L implies b [= a ` ) :: thesis: ( b [= a ` implies b "/\" a = Bottom L )

proof

assume A1: b "/\" a = Bottom L ; :: thesis: b [= a `
b = b "/\" (Top L)
.= b "/\" (a "\/" (a `)) by Th19
.= (Bottom L) "\/" (b "/\" (a `)) by A1, Def11
.= b "/\" (a `) ;
then b "\/" (a `) = a ` by Def8;
hence b [= a ` ; :: thesis: verum

end;

thus ( b [= a ` implies b "/\" a = Bottom L ) :: thesis: verum

proof

assume b [= a ` ; :: thesis: b "/\" a = Bottom L
then b "/\" a [= (a `) "/\" a by Th7;
then A2: b "/\" a [= Bottom L by Th18;
Bottom L [= b "/\" a ;
hence b "/\" a = Bottom L by A2, Th6; :: thesis: verum

end;