let A, B, A1, B1 be set ; :: thesis: ( A misses B & A1 c= A & B1 c= B & A1 \/ B1 = A \/ B implies ( A1 = A & B1 = B ) )
assume A1: A misses B ; :: thesis: ( not A1 c= A or not B1 c= B or not A1 \/ B1 = A \/ B or ( A1 = A & B1 = B ) )
assume A2: ( A1 c= A & B1 c= B ) ; :: thesis: ( not A1 \/ B1 = A \/ B or ( A1 = A & B1 = B ) )
assume A3: A1 \/ B1 = A \/ B ; :: thesis: ( A1 = A & B1 = B )
A4: A c= A1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A1 )
assume A5: x in A ; :: thesis: x in A1
then A6: x in A \/ B by XBOOLE_0:def 3;
not x in B1

proof

assume x in B1 ; :: thesis: contradiction
then x in A /\ B by A5, XBOOLE_0:def 4, A2;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

hence x in A1 by A6, XBOOLE_0:def 3, A3; :: thesis: verum

end;

B c= B1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in B1 )
assume A7: x in B ; :: thesis: x in B1
then A8: x in A \/ B by XBOOLE_0:def 3;
not x in A1

proof

assume x in A1 ; :: thesis: contradiction
then x in A /\ B by A7, XBOOLE_0:def 4, A2;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

hence x in B1 by A8, XBOOLE_0:def 3, A3; :: thesis: verum

end;

hence ( A1 = A & B1 = B ) by A2, XBOOLE_0:def 10, A4; :: thesis: verum