let SFX, SFY be set ; :: thesis: union (INTERSECTION (SFX,SFY)) = (union SFX) /\ (union SFY)
thus union (INTERSECTION (SFX,SFY)) c= (union SFX) /\ (union SFY) :: according to XBOOLE_0:def 10 :: thesis: (union SFX) /\ (union SFY) c= union (INTERSECTION (SFX,SFY))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (INTERSECTION (SFX,SFY)) or x in (union SFX) /\ (union SFY) )
assume x in union (INTERSECTION (SFX,SFY)) ; :: thesis: x in (union SFX) /\ (union SFY)
then consider Z being set such that
A1: x in Z and
A2: Z in INTERSECTION (SFX,SFY) by TARSKI:def 4;
consider X, Y being set such that
A3: X in SFX and
A4: Y in SFY and
A5: Z = X /\ Y by A2, Def5;
x in Y by A1, A5, XBOOLE_0:def 4;
then A6: x in union SFY by A4, TARSKI:def 4;
x in X by A1, A5, XBOOLE_0:def 4;
then x in union SFX by A3, TARSKI:def 4;
hence x in (union SFX) /\ (union SFY) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union SFX) /\ (union SFY) or x in union (INTERSECTION (SFX,SFY)) )
assume A7: x in (union SFX) /\ (union SFY) ; :: thesis: x in union (INTERSECTION (SFX,SFY))
then x in union SFX by XBOOLE_0:def 4;
then consider X0 being set such that
A8: ( x in X0 & X0 in SFX ) by TARSKI:def 4;
x in union SFY by A7, XBOOLE_0:def 4;
then consider Y0 being set such that
A9: ( x in Y0 & Y0 in SFY ) by TARSKI:def 4;
( X0 /\ Y0 in INTERSECTION (SFX,SFY) & x in X0 /\ Y0 ) by A8, A9, Def5, XBOOLE_0:def 4;
hence x in union (INTERSECTION (SFX,SFY)) by TARSKI:def 4; :: thesis: verum