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 set ; :: 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 & Z in INTERSECTION SFX,SFY ) by TARSKI:def 4;
consider X, Y being set such that
A2: ( X in SFX & Y in SFY & Z = X /\ Y ) by A1, Def5;
( x in X & x in Y ) by A1, A2, XBOOLE_0:def 4;
then ( x in union SFX & x in union SFY ) by A2, TARSKI:def 4;
hence x in (union SFX) /\ (union SFY) by XBOOLE_0:def 4; :: thesis: verum

end;

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