let SFX, SFY be set ; :: thesis: ( SFX <> {} & SFY <> {} implies (meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY)) )
set y = the Element of SFX;
set z = the Element of SFY;
assume ( SFX <> {} & SFY <> {} ) ; :: thesis: (meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY))
then A1: the Element of SFX \/ the Element of SFY in UNION (SFX,SFY) by Def4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (meet SFX) \/ (meet SFY) or x in meet (UNION (SFX,SFY)) )
assume x in (meet SFX) \/ (meet SFY) ; :: thesis: x in meet (UNION (SFX,SFY))
then A2: ( x in meet SFX or x in meet SFY ) by XBOOLE_0:def 3;
for Z being set st Z in UNION (SFX,SFY) holds
x in Z
proof
let Z be set ; :: thesis: ( Z in UNION (SFX,SFY) implies x in Z )
assume Z in UNION (SFX,SFY) ; :: thesis: x in Z
then consider X, Y being set such that
A3: ( X in SFX & Y in SFY ) and
A4: Z = X \/ Y by Def4;
( x in X or x in Y ) by A2, A3, Def1;
hence x in Z by A4, XBOOLE_0:def 3; :: thesis: verum
end;
hence x in meet (UNION (SFX,SFY)) by A1, Def1; :: thesis: verum