let x1, y1, x2, y2 be set ; :: thesis: ( x1 U+ y1 c= x2 U+ y2 iff ( x1 c= x2 & y1 c= y2 ) )

hereby :: thesis: ( x1 c= x2 & y1 c= y2 implies x1 U+ y1 c= x2 U+ y2 )

assume A1: x1 U+ y1 c= x2 U+ y2 ; :: thesis: ( x1 c= x2 & y1 c= y2 )
thus x1 c= x2 :: thesis: y1 c= y2

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x1 or a in x2 )
assume a in x1 ; :: thesis: a in x2
then [a,1] in x1 U+ y1 by Th76;
hence a in x2 by A1, Th76; :: thesis: verum

end;

thus y1 c= y2 :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in y1 or a in y2 )
assume a in y1 ; :: thesis: a in y2
then [a,2] in x1 U+ y1 by Th77;
hence a in y2 by A1, Th77; :: thesis: verum

end;

end;

assume A2: ( x1 c= x2 & y1 c= y2 ) ; :: thesis: x1 U+ y1 c= x2 U+ y2
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x1 U+ y1 or a in x2 U+ y2 )
assume A3: a in x1 U+ y1 ; :: thesis: a in x2 U+ y2
then A4: ( ( a `2 = 1 & a `1 in x1 ) or ( a `2 = 2 & a `1 in y1 ) ) by Th75;
a = [(a `1),(a `2)] by A3, Th75;
hence a in x2 U+ y2 by A2, A4, Th76, Th77; :: thesis: verum