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

proof

thus
{[{},{}]} c= DISJOINT_PAIRS {}
:: thesis: verum
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;assume x in DISJOINT_PAIRS {} ; :: thesis: x in {[{},{}]}

then x = [{},{}] by Th15;

hence x in {[{},{}]} by TARSKI:def 1; :: 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;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