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

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

hence
x in meet (UNION (SFX,SFY))
by A1, Def1; :: thesis: verum
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;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