let I be non empty set ; :: thesis: Class (nabla I) = {I}
thus Class (nabla I) c= {I} by Th4; :: according to XBOOLE_0:def 10 :: thesis: {I} c= Class (nabla I)
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in {I} or q in Class (nabla I) )
assume q in {I} ; :: thesis: q in Class (nabla I)
then A1: q = I by TARSKI:def 1;
consider a being set such that
A2: a in I by XBOOLE_0:def 1;
Class (nabla I),a = I by A2, EQREL_1:34;
hence q in Class (nabla I) by A1, A2, EQREL_1:def 5; :: thesis: verum