defpred S₁[ set ] means ( $1 is infinite & $1 is limit_ordinal & sup (X /\ $1) = $1 );
thus { B1 where B1 is Element of A : S₁[B1] } is Subset of A from DOMAIN_1:sch 7(); :: thesis: verum