let G be finite Group; :: thesis: for H1, H2 being strict Subgroup of G st card (H1 /\ H2) = card H1 & card (H1 /\ H2) = card H2 holds
H1 = H2
let H1, H2 be strict Subgroup of G; :: thesis: ( card (H1 /\ H2) = card H1 & card (H1 /\ H2) = card H2 implies H1 = H2 )
assume A1: card (H1 /\ H2) = card H1 ; :: thesis: ( not card (H1 /\ H2) = card H2 or H1 = H2 )
assume A2: card (H1 /\ H2) = card H2 ; :: thesis: H1 = H2
A3: H1 /\ H2 = H1

proof

reconsider H12 = H1 /\ H2 as strict Subgroup of H1 by GROUP_2:88;
multMagma(# the carrier of H12, the multF of H12 #) = multMagma(# the carrier of H1, the multF of H1 #) by A1, GROUP_2:73;
hence H1 /\ H2 = H1 ; :: thesis: verum

end;

H1 /\ H2 = H2

proof

reconsider H12 = H1 /\ H2 as strict Subgroup of H2 by GROUP_2:88;
multMagma(# the carrier of H12, the multF of H12 #) = multMagma(# the carrier of H2, the multF of H2 #) by A2, GROUP_2:73;
hence H1 /\ H2 = H2 ; :: thesis: verum

end;

hence H1 = H2 by A3; :: thesis: verum