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 )
proof
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;
assume A1: ( X meets Y or X meets Z ) ; :: thesis: X meets Y "\/" Z
per cases ( X meets Y or X meets Z ) by A1;
suppose A2: X meets Y ; :: thesis: X meets Y "\/" Z
X "/\" Y [= (X "/\" Y) "\/" (X "/\" Z) by LATTICES:5;
then A3: X "/\" Y [= X "/\" (Y "\/" Z) by LATTICES:def 11;
X "/\" (Y "\/" Z) <> Bottom L by A3, Th9, A2;
hence X meets Y "\/" Z ; :: thesis: verum
end;
suppose A4: X meets Z ; :: thesis: X meets Y "\/" Z
A5: (X "/\" Z) "\/" (X "/\" Y) = X "/\" (Y "\/" Z) by LATTICES:def 11;
X "/\" Z <> Bottom L by A4;
then X "/\" (Y "\/" Z) <> Bottom L by A5, Th11;
hence X meets Y "\/" Z ; :: thesis: verum
end;
end;