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))

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

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 SFX) /\ (union SFY) or x in union (INTERSECTION (SFX,SFY)) )
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;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

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