let G be non trivial Group; :: thesis: for H being proper Subgroup of G
for K being Subgroup of G st H is Subgroup of K & multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of K, the multF of K #) holds
K is non trivial Subgroup of G
let H be proper Subgroup of G; :: thesis: for K being Subgroup of G st H is Subgroup of K & multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of K, the multF of K #) holds
K is non trivial Subgroup of G
let K be Subgroup of G; :: thesis: ( H is Subgroup of K & multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of K, the multF of K #) implies K is non trivial Subgroup of G )
assume A1: H is Subgroup of K ; :: thesis: ( not multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of K, the multF of K #) or K is non trivial Subgroup of G )
assume A2: multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of K, the multF of K #) ; :: thesis: K is non trivial Subgroup of G
assume B1: K is not non trivial Subgroup of G ; :: thesis: contradiction
then H is trivial Subgroup of G by A1, Th9;
hence contradiction by A2, B1, Th8; :: thesis: verum