hereby :: thesis: ( a is not Object of C implies ex b₁ being set st b₁ = {} )

assume a is Object of C ; :: thesis: ex x being set ex b being Object of C st
( b = a & x = proj1 (idm b) )
then reconsider b = a as Object of C ;
take x = proj1 (idm b); :: thesis: ex b being Object of C st
( b = a & x = proj1 (idm b) )
take b = b; :: thesis: ( b = a & x = proj1 (idm b) )
thus ( b = a & x = proj1 (idm b) ) ; :: thesis: verum

end;

thus ( a is not Object of C implies ex b₁ being set st b₁ = {} ) ; :: thesis: verum