defpred S₁[ set ] means ex a being Element of G st $1 = H + a;
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 ) ) & ( for A being Subset of G holds
( A in F2 iff ex a being Element of G st A = H + a ) ) implies F1 = F2 )
assume A3: for A being Subset of G holds
( A in F1 iff S₁[A] ) ; :: thesis: ( ex A being Subset of G st
( ( A in F2 implies ex a being Element of G st A = H + a ) implies ( ex a being Element of G st A = H + a & not A in F2 ) ) or F1 = F2 )
assume A4: for A being Subset of G holds
( A in F2 iff S₁[A] ) ; :: thesis: F1 = F2
thus F1 = F2 from SUBSET_1:sch 4(A3, A4); :: thesis: verum