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

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

B c= B1
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

end;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

hence
x in A1
by A6, XBOOLE_0:def 3, A3; :: thesis: verum
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;then x in A /\ B by A5, XBOOLE_0:def 4, A2;

hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

proof

hence
( A1 = A & B1 = B )
by A2, XBOOLE_0:def 10, A4; :: thesis: verum
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

end;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

hence
x in B1
by A8, XBOOLE_0:def 3, A3; :: thesis: verum
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;then x in A /\ B by A7, XBOOLE_0:def 4, A2;

hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum