let G be Group; :: thesis: for K being trivial Subgroup of G
for H being Subgroup of G st H is Subgroup of K holds
H is trivial Subgroup of G
let K be trivial Subgroup of G; :: thesis: for H being Subgroup of G st H is Subgroup of K holds
H is trivial Subgroup of G
let H be Subgroup of G; :: thesis: ( H is Subgroup of K implies H is trivial Subgroup of G )
assume A1: H is Subgroup of K ; :: thesis: H is trivial Subgroup of G
the carrier of H = {(1_ G)}

proof

multMagma(# the carrier of K, the multF of K #) = (1). G by Th7;
then the carrier of K = {(1_ G)} by GROUP_2:def 7;
then B1: the carrier of H c= {(1_ G)} by A1, GROUP_2:def 5;
(1). G is Subgroup of H by GROUP_2:65;
then the carrier of ((1). G) c= the carrier of H by GROUP_2:def 5;
then {(1_ G)} c= the carrier of H by GROUP_2:def 7;
hence the carrier of H = {(1_ G)} by B1, XBOOLE_0:def 10; :: thesis: verum

end;

hence H is trivial Subgroup of G ; :: thesis: verum