let G be Group; :: thesis: for H, K being strict Subgroup of G st H <> K & K is Subgroup of H holds
ex g being Element of G st
( g in H & not g in K )
let H, K be strict Subgroup of G; :: thesis: ( H <> K & K is Subgroup of H implies ex g being Element of G st
( g in H & not g in K ) )
assume A1: H <> K ; :: thesis: ( not K is Subgroup of H or ex g being Element of G st
( g in H & not g in K ) )
assume A2: K is Subgroup of H ; :: thesis: ex g being Element of G st
( g in H & not g in K )
then H is not Subgroup of K by A1, GROUP_2:55;
then ( the carrier of K c= the carrier of H & the carrier of H <> the carrier of K ) by A2, GROUP_2:def 5, GROUP_2:57;
then consider x being object such that
A3: ( x in the carrier of H & not x in the carrier of K ) by XBOOLE_0:6, XBOOLE_0:def 8;
( x in H & not x in K ) by A3;
then x in G by GROUP_2:40;
then reconsider g = x as Element of G ;
take g ; :: thesis: ( g in H & not g in K )
thus ( g in H & not g in K ) by A3; :: thesis: verum