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 A1: X "\/" Y = Bottom L ; :: thesis: ( X = Bottom L & Y = Bottom L )
then A2: ( X [= Bottom L & Bottom L [= X ) by LATTICES:22, LATTICES:41;
( Y [= Bottom L & Bottom L [= Y ) by A1, LATTICES:22, LATTICES:41;
hence ( X = Bottom L & Y = Bottom L ) by A2, Def3; :: thesis: verum

end;

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