let I be set ; :: thesis: Class (nabla I) c= {I}
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Class (nabla I) or q in {I} )
assume q in Class (nabla I) ; :: thesis: q in {I}
then consider x being object such that
A1: x in I and
A2: q = Class ((nabla I),x) by EQREL_1:def 3;
Class ((nabla I),x) = I by A1, EQREL_1:26;
hence q in {I} by A2, TARSKI:def 1; :: thesis: verum