thus PARTITIONS {} c= {{}} :: according to XBOOLE_0:def 10 :: thesis: {{}} c= PARTITIONS {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PARTITIONS {} or x in {{}} )
assume x in PARTITIONS {} ; :: thesis: x in {{}}
then x is a_partition of {} by PARTIT1:def 3;
then x = {} ;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{}} or x in PARTITIONS {} )
{} in PARTITIONS {} by EQREL_1:45, PARTIT1:def 3;
hence ( not x in {{}} or x in PARTITIONS {} ) by TARSKI:def 1; :: thesis: verum