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