defpred S₁[ set , set ] means verum;
let G be strict Group; :: thesis: for B being strict Subgroup of G holds
( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B )
let B be strict Subgroup of G; :: thesis: ( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B )
thus ( G ` is Subgroup of B implies for a, b being Element of G holds [.a,b.] in B ) by GROUP_2:40, GROUP_5:74; :: thesis: ( ( for a, b being Element of G holds [.a,b.] in B ) implies G ` is Subgroup of B )
deffunc H₁( Element of G, Element of G) -> Element of the carrier of G = [.$1,$2.];
reconsider X = { H₁(a,b) where a, b is Element of G : S₁[a,b] } as Subset of G from DOMAIN_1:sch 9();
assume A1: for a, b being Element of G holds [.a,b.] in B ; :: thesis: G ` is Subgroup of B
X c= the carrier of B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in the carrier of B )
assume x in X ; :: thesis: x in the carrier of B
then ex a, b being Element of G st x = [.a,b.] ;
then x in B by A1;
hence x in the carrier of B ; :: thesis: verum

end;

then gr X is Subgroup of B by GROUP_4:def 4;
hence G ` is Subgroup of B by Th6; :: thesis: verum