let G be strict Group; :: thesis: for a, b being Element of G holds [.a,b.] in G `
let a, b be Element of G; :: thesis: [.a,b.] in G `
( a in (Omega). G & b in (Omega). G ) by STRUCT_0:def 5;
hence [.a,b.] in G ` by Th65; :: thesis: verum