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)

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

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

( meet (X \/ Y) c= meet X & meet (X \/ Y) c= meet Y )
by A1, A2, Th6, XBOOLE_1:7;
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;

end;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

hence
x in meet (X \/ Y)
by A1, Def1; :: thesis: verumx 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;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

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