let X, Y be set ; :: thesis: ( X <> {} & Y <> {} implies meet (X \/ Y) = (meet X) /\ (meet Y) )
assume that
A1: X <> {} and
A2: Y <> {} ; :: thesis: meet (X \/ Y) = (meet X) /\ (meet Y)
A3: (meet X) /\ (meet Y) c= meet (X \/ Y)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (meet X) /\ (meet Y) or x in meet (X \/ Y) )
assume x in (meet X) /\ (meet Y) ; :: thesis: x in meet (X \/ Y)
then A4: ( x in meet X & x in meet Y ) by XBOOLE_0:def 4;

now :: thesis: for Z being set st Z in X \/ Y holds
x in Z

let Z be set ; :: thesis: ( Z in X \/ Y implies x in Z )
assume Z in X \/ Y ; :: thesis: x in Z
then ( Z in X or Z in Y ) by XBOOLE_0:def 3;
hence x in Z by A4, Def1; :: thesis: verum

end;

hence x in meet (X \/ Y) by A1, Def1; :: thesis: verum

end;

( meet (X \/ Y) c= meet X & meet (X \/ Y) c= meet Y ) by A1, A2, Th6, XBOOLE_1:7;
then meet (X \/ Y) c= (meet X) /\ (meet Y) by XBOOLE_1:19;
hence meet (X \/ Y) = (meet X) /\ (meet Y) by A3; :: thesis: verum