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

proof

let x be set ; :: 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 Th20;
hence x in {[{} ,{} ]} by TARSKI:def 1; :: thesis: verum

end;

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

proof

let x be set ; :: 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 Th17;
hence x in DISJOINT_PAIRS {} ; :: thesis: verum

end;