defpred S1[ set ] means ex a being Element of G st $1 = a + H;
let F1, F2 be Subset-Family of G; ( ( for A being Subset of G holds
( A in F1 iff ex a being Element of G st A = a + H ) ) & ( for A being Subset of G holds
( A in F2 iff ex a being Element of G st A = a + H ) ) implies F1 = F2 )
assume A1:
for A being Subset of G holds
( A in F1 iff S1[A] )
; ( ex A being Subset of G st
( ( A in F2 implies ex a being Element of G st A = a + H ) implies ( ex a being Element of G st A = a + H & not A in F2 ) ) or F1 = F2 )
assume A2:
for A being Subset of G holds
( A in F2 iff S1[A] )
; F1 = F2
thus
F1 = F2
from SUBSET_1:sch 4(A1, A2); verum