let L be B_Lattice; :: thesis: for X, Y, Z being Element of L holds

( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )

let X, Y, Z be Element of L; :: thesis: ( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )

thus ( not X meets Y "\/" Z or X meets Y or X meets Z ) :: thesis: ( ( X meets Y or X meets Z ) implies X meets Y "\/" Z )

( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )

let X, Y, Z be Element of L; :: thesis: ( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )

thus ( not X meets Y "\/" Z or X meets Y or X meets Z ) :: thesis: ( ( X meets Y or X meets Z ) implies X meets Y "\/" Z )

proof

assume A1:
( X meets Y or X meets Z )
; :: thesis: X meets Y "\/" Z
assume
X meets Y "\/" Z
; :: thesis: ( X meets Y or X meets Z )

then X "/\" (Y "\/" Z) <> Bottom L ;

then (X "/\" Y) "\/" (X "/\" Z) <> Bottom L by LATTICES:def 11;

then ( X "/\" Y <> Bottom L or X "/\" Z <> Bottom L ) ;

hence ( X meets Y or X meets Z ) ; :: thesis: verum

end;then X "/\" (Y "\/" Z) <> Bottom L ;

then (X "/\" Y) "\/" (X "/\" Z) <> Bottom L by LATTICES:def 11;

then ( X "/\" Y <> Bottom L or X "/\" Z <> Bottom L ) ;

hence ( X meets Y or X meets Z ) ; :: thesis: verum

per cases
( X meets Y or X meets Z )
by A1;

end;