let SFX, SFY be set ; union (INTERSECTION (SFX,SFY)) = (union SFX) /\ (union SFY)
thus
union (INTERSECTION (SFX,SFY)) c= (union SFX) /\ (union SFY)
XBOOLE_0:def 10 (union SFX) /\ (union SFY) c= union (INTERSECTION (SFX,SFY))proof
let x be
object ;
TARSKI:def 3 ( not x in union (INTERSECTION (SFX,SFY)) or x in (union SFX) /\ (union SFY) )
assume
x in union (INTERSECTION (SFX,SFY))
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in (union SFX) /\ (union SFY) or x in union (INTERSECTION (SFX,SFY)) )
assume A7:
x in (union SFX) /\ (union SFY)
; 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; verum