let x, y, z be set ; :: thesis: ( z c= x U+ y implies ex x1, y1 being set st
( z = x1 U+ y1 & x1 c= x & y1 c= y ) )
assume A1: z c= x U+ y ; :: thesis: ex x1, y1 being set st
( z = x1 U+ y1 & x1 c= x & y1 c= y )
take x1 = proj1 (z /\ [:x,{1}:]); :: thesis: ex y1 being set st
( z = x1 U+ y1 & x1 c= x & y1 c= y )
take y1 = proj1 (z /\ [:y,{2}:]); :: thesis: ( z = x1 U+ y1 & x1 c= x & y1 c= y )
A2: x U+ y = [:x,{1}:] \/ [:y,{2}:] by Th73;
thus z = x1 U+ y1 :: thesis: ( x1 c= x & y1 c= y )
proof
hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: x1 U+ y1 c= z
let a be object ; :: thesis: ( a in z implies a in x1 U+ y1 )
assume A3: a in z ; :: thesis: a in x1 U+ y1
then A4: a = [(a `1),(a `2)] by A1, Th75;
( a in [:x,{1}:] or a in [:y,{2}:] ) by A1, A2, A3, XBOOLE_0:def 3;
then ( ( a in z /\ [:x,{1}:] & a `2 = 1 ) or ( a in z /\ [:y,{2}:] & a `2 = 2 ) ) by A3, A4, XBOOLE_0:def 4, ZFMISC_1:106;
then ( ( a `1 in x1 & a `2 = 1 ) or ( a `1 in y1 & a `2 = 2 ) ) by A4, XTUPLE_0:def 12;
hence a in x1 U+ y1 by A4, Th76, Th77; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x1 U+ y1 or a in z )
assume A5: a in x1 U+ y1 ; :: thesis: a in z
then A6: a = [(a `1),(a `2)] by Th75;
per cases ( ( a `2 = 1 & a `1 in x1 ) or ( a `2 = 2 & a `1 in y1 ) ) by A5, Th75;
suppose A7: ( a `2 = 1 & a `1 in x1 ) ; :: thesis: a in z
then consider b being object such that
A8: [(a `1),b] in z /\ [:x,{1}:] by XTUPLE_0:def 12;
( [(a `1),b] in z & [(a `1),b] in [:x,{1}:] ) by A8, XBOOLE_0:def 4;
hence a in z by A6, A7, ZFMISC_1:106; :: thesis: verum
end;
suppose A9: ( a `2 = 2 & a `1 in y1 ) ; :: thesis: a in z
then consider b being object such that
A10: [(a `1),b] in z /\ [:y,{2}:] by XTUPLE_0:def 12;
( [(a `1),b] in z & [(a `1),b] in [:y,{2}:] ) by A10, XBOOLE_0:def 4;
hence a in z by A6, A9, ZFMISC_1:106; :: thesis: verum
end;
end;
end;
z /\ [:y,{2}:] c= [:y,{2}:] by XBOOLE_1:17;
then A11: y1 c= proj1 [:y,{2}:] by XTUPLE_0:8;
z /\ [:x,{1}:] c= [:x,{1}:] by XBOOLE_1:17;
then x1 c= proj1 [:x,{1}:] by XTUPLE_0:8;
hence ( x1 c= x & y1 c= y ) by A11, FUNCT_5:9; :: thesis: verum