let X be set ; ( X <> {} implies { x where x is Element of X : verum } = X )
assume
X <> {}
; { x where x is Element of X : verum } = X
then reconsider XX = X as non empty set ;
defpred S1[ set ] means verum;
A1:
for x being set st x in XX holds
S1[x]
;
set Y = { x where x is Element of XX : S1[x] } ;
XX = { x where x is Element of XX : S1[x] }
from FOMODEL0:sch 6(A1);
hence
{ x where x is Element of X : verum } = X
; verum