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