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

assume a is object of ; :: thesis: ex x being set ex b being object of st
( b = a & x = proj1 (idm b) )
then reconsider b = a as object of ;
take x = proj1 (idm b); :: thesis: ex b being object of 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 implies ex b₁ being set st b₁ = {} ) ; :: thesis: verum