defpred S_{1}[ set ] means ex a being Element of G st $1 = (H * a) * K;

ex F being Subset-Family of G st

for A being Subset of G holds

( A in F iff S_{1}[A] )
from SUBSET_1:sch 3();

hence ex b_{1} being Subset-Family of G st

for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = (H * a) * K )
; :: thesis: verum

ex F being Subset-Family of G st

for A being Subset of G holds

( A in F iff S

hence ex b

for A being Subset of G holds

( A in b