let x, y be object ; :: thesis: for X, Y being set holds Ext ((X \/ Y),x,y) = (Ext (X,x,y)) \/ (Ext (Y,x,y))
let X, Y be set ; :: thesis: Ext ((X \/ Y),x,y) = (Ext (X,x,y)) \/ (Ext (Y,x,y))
thus Ext ((X \/ Y),x,y) c= (Ext (X,x,y)) \/ (Ext (Y,x,y)) :: according to XBOOLE_0:def 10 :: thesis: (Ext (X,x,y)) \/ (Ext (Y,x,y)) c= Ext ((X \/ Y),x,y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ext ((X \/ Y),x,y) or a in (Ext (X,x,y)) \/ (Ext (Y,x,y)) )
assume a in Ext ((X \/ Y),x,y) ; :: thesis: a in (Ext (X,x,y)) \/ (Ext (Y,x,y))

per cases then ( a in { (A \/ {y}) where A is Element of X \/ Y : x in A } or a in { A where A is Element of X \/ Y : ( not x in A & A in X \/ Y ) } ) by XBOOLE_0:def 3;

suppose a in { (A \/ {y}) where A is Element of X \/ Y : x in A } ; :: thesis: a in (Ext (X,x,y)) \/ (Ext (Y,x,y))

then consider A being Element of X \/ Y such that
A1: ( a = A \/ {y} & x in A ) ;
X \/ Y <> {} by A1, SUBSET_1:def 1;
then ( A in X or A in Y ) by XBOOLE_0:def 3;
then ( a in { (A \/ {y}) where A is Element of X : x in A } or a in { (A \/ {y}) where A is Element of Y : x in A } ) by A1;
then ( a in Ext (X,x,y) or a in Ext (Y,x,y) ) by XBOOLE_0:def 3;
hence a in (Ext (X,x,y)) \/ (Ext (Y,x,y)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose a in { A where A is Element of X \/ Y : ( not x in A & A in X \/ Y ) } ; :: thesis: a in (Ext (X,x,y)) \/ (Ext (Y,x,y))

then consider A being Element of X \/ Y such that
A2: ( a = A & not x in A & A in X \/ Y ) ;
( A in X or A in Y ) by A2, XBOOLE_0:def 3;
then ( a in { A where A is Element of X : ( not x in A & A in X ) } or a in { A where A is Element of Y : ( not x in A & A in Y ) } ) by A2;
then ( a in Ext (X,x,y) or a in Ext (Y,x,y) ) by XBOOLE_0:def 3;
hence a in (Ext (X,x,y)) \/ (Ext (Y,x,y)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A3: Ext (X,x,y) c= Ext ((X \/ Y),x,y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ext (X,x,y) or a in Ext ((X \/ Y),x,y) )
assume a in Ext (X,x,y) ; :: thesis: a in Ext ((X \/ Y),x,y)

per cases then ( a in { (A \/ {y}) where A is Element of X : x in A } or a in { A where A is Element of X : ( not x in A & A in X ) } ) by XBOOLE_0:def 3;

suppose a in { (A \/ {y}) where A is Element of X : x in A } ; :: thesis: a in Ext ((X \/ Y),x,y)

then consider A being Element of X such that
A4: ( a = A \/ {y} & x in A ) ;
X <> {} by A4, SUBSET_1:def 1;
then A in X \/ Y by XBOOLE_0:def 3;
then a in { (A \/ {y}) where A is Element of X \/ Y : x in A } by A4;
hence a in Ext ((X \/ Y),x,y) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose a in { A where A is Element of X : ( not x in A & A in X ) } ; :: thesis: a in Ext ((X \/ Y),x,y)

then consider A being Element of X such that
A5: ( a = A & not x in A & A in X ) ;
A in X \/ Y by A5, XBOOLE_0:def 3;
then a in { A where A is Element of X \/ Y : ( not x in A & A in X \/ Y ) } by A5;
hence a in Ext ((X \/ Y),x,y) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

Ext (Y,x,y) c= Ext ((X \/ Y),x,y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ext (Y,x,y) or a in Ext ((X \/ Y),x,y) )
assume a in Ext (Y,x,y) ; :: thesis: a in Ext ((X \/ Y),x,y)

per cases then ( a in { (A \/ {y}) where A is Element of Y : x in A } or a in { A where A is Element of Y : ( not x in A & A in Y ) } ) by XBOOLE_0:def 3;

suppose a in { (A \/ {y}) where A is Element of Y : x in A } ; :: thesis: a in Ext ((X \/ Y),x,y)

then consider A being Element of Y such that
A6: ( a = A \/ {y} & x in A ) ;
Y <> {} by A6, SUBSET_1:def 1;
then A in X \/ Y by XBOOLE_0:def 3;
then a in { (A \/ {y}) where A is Element of X \/ Y : x in A } by A6;
hence a in Ext ((X \/ Y),x,y) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose a in { A where A is Element of Y : ( not x in A & A in Y ) } ; :: thesis: a in Ext ((X \/ Y),x,y)

then consider A being Element of Y such that
A7: ( a = A & not x in A & A in Y ) ;
A in X \/ Y by A7, XBOOLE_0:def 3;
then a in { A where A is Element of X \/ Y : ( not x in A & A in X \/ Y ) } by A7;
hence a in Ext ((X \/ Y),x,y) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence (Ext (X,x,y)) \/ (Ext (Y,x,y)) c= Ext ((X \/ Y),x,y) by A3, XBOOLE_1:8; :: thesis: verum