let L be 0_Lattice; :: thesis: for X, Y being Element of L holds
( X "\/" Y = Bottom L iff ( X = Bottom L & Y = Bottom L ) )
let X, Y be Element of L; :: thesis: ( X "\/" Y = Bottom L iff ( X = Bottom L & Y = Bottom L ) )
thus ( X "\/" Y = Bottom L implies ( X = Bottom L & Y = Bottom L ) ) :: thesis: ( X = Bottom L & Y = Bottom L implies X "\/" Y = Bottom L )

proof

assume X "\/" Y = Bottom L ; :: thesis: ( X = Bottom L & Y = Bottom L )
then A1: ( X [= Bottom L & Y [= Bottom L ) by LATTICES:22;
( Bottom L [= X & Bottom L [= Y ) by LATTICES:41;
hence ( X = Bottom L & Y = Bottom L ) by A1, Def3; :: thesis: verum

end;

thus ( X = Bottom L & Y = Bottom L implies X "\/" Y = Bottom L ) by LATTICES:39; :: thesis: verum