thus DISJOINT_PAIRS {} c= {[{},{}]} :: according to XBOOLE_0:def 10 :: thesis: {[{},{}]} c= DISJOINT_PAIRS {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in DISJOINT_PAIRS {} or x in {[{},{}]} )
assume x in DISJOINT_PAIRS {} ; :: thesis: x in {[{},{}]}
then x = [{},{}] by Th15;
hence x in {[{},{}]} by TARSKI:def 1; :: thesis: verum

end;

thus {[{},{}]} c= DISJOINT_PAIRS {} :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[{},{}]} or x in DISJOINT_PAIRS {} )
assume x in {[{},{}]} ; :: thesis: x in DISJOINT_PAIRS {}
then x = [{},{}] by TARSKI:def 1;
then x is Element of DISJOINT_PAIRS {} by Th12;
hence x in DISJOINT_PAIRS {} ; :: thesis: verum

end;