defpred S₁[ set ] means ex a being Element of G st $1 = H * a;
ex F being Subset-Family of G st
for A being Subset of G holds
( A in F iff S₁[A] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset-Family of G st
for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = H * a ) ; :: thesis: verum