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 ;
x in Y by ;
then A6: x in union SFY by ;
x in X by ;
then x in union SFX by ;
hence x in (union SFX) /\ (union SFY) by ; :: 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 ;
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 ;
hence x in union (INTERSECTION (SFX,SFY)) by TARSKI:def 4; :: thesis: verum