let F1, F2 be Subset-Family of G; :: thesis: ( ( for A being Subset of G holds

( A in F1 iff ex a being Element of G st A = (H * a) * K ) ) & ( for A being Subset of G holds

( A in F2 iff ex a being Element of G st A = (H * a) * K ) ) implies F1 = F2 )

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

assume A1: for A being Subset of G holds

( A in F1 iff S_{1}[A] )
; :: thesis: ( ex A being Subset of G st

( ( A in F2 implies ex a being Element of G st A = (H * a) * K ) implies ( ex a being Element of G st A = (H * a) * K & not A in F2 ) ) or F1 = F2 )

assume A2: for A being Subset of G holds

( A in F2 iff S_{1}[A] )
; :: thesis: F1 = F2

thus F1 = F2 from SUBSET_1:sch 4(A1, A2); :: thesis: verum

( A in F1 iff ex a being Element of G st A = (H * a) * K ) ) & ( for A being Subset of G holds

( A in F2 iff ex a being Element of G st A = (H * a) * K ) ) implies F1 = F2 )

defpred S

assume A1: for A being Subset of G holds

( A in F1 iff S

( ( A in F2 implies ex a being Element of G st A = (H * a) * K ) implies ( ex a being Element of G st A = (H * a) * K & not A in F2 ) ) or F1 = F2 )

assume A2: for A being Subset of G holds

( A in F2 iff S

thus F1 = F2 from SUBSET_1:sch 4(A1, A2); :: thesis: verum