let x1, y1, x2, y2 be set ; :: thesis: ( x1 U+ y1 = x2 U+ y2 iff ( x1 = x2 & y1 = y2 ) )
A1: ( x1 U+ y1 c= x2 U+ y2 iff ( x1 c= x2 & y1 c= y2 ) ) by Th79;
( x2 U+ y2 c= x1 U+ y1 iff ( x2 c= x1 & y2 c= y1 ) ) by Th79;
hence ( x1 U+ y1 = x2 U+ y2 iff ( x1 = x2 & y1 = y2 ) ) by A1, XBOOLE_0:def 10; :: thesis: verum