let G be Group; :: thesis: for A, B being Subset of G st A c= B holds
gr A is Subgroup of gr B
let A, B be Subset of G; :: thesis: ( A c= B implies gr A is Subgroup of gr B )
assume A1: A c= B ; :: thesis: gr A is Subgroup of gr B
now :: thesis: for a being Element of G st a in gr A holds
a in gr B
let a be Element of G; :: thesis: ( a in gr A implies a in gr B )
assume a in gr A ; :: thesis: a in gr B
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A2: len F = len I and
A3: rng F c= A and
A4: Product (F |^ I) = a by Th28;
rng F c= B by A1, A3;
hence a in gr B by A2, A4, Th28; :: thesis: verum
end;
hence gr A is Subgroup of gr B by GROUP_2:58; :: thesis: verum