let p be Nat; :: thesis: for G being finite Group
for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds
gr {x} = gr {d}
let G be finite Group; :: thesis: for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds
gr {x} = gr {d}
let x, d be Element of G; :: thesis: ( ord d = p & p is prime & x in gr {d} & not x = 1_ G implies gr {x} = gr {d} )
assume A1: ( ord d = p & p is prime ) ; :: thesis: ( not x in gr {d} or x = 1_ G or gr {x} = gr {d} )
assume x in gr {d} ; :: thesis: ( x = 1_ G or gr {x} = gr {d} )
then X1: gr {x} is strict Subgroup of gr {d} by GRCY212;
X2: card (gr {d}) = p by A1, GR_CY_1:7;
( gr {x} = (1). (gr {d}) implies x = 1_ G )
proof
assume X3: gr {x} = (1). (gr {d}) ; :: thesis: x = 1_ G
x in the carrier of (gr {x}) by GR_CY_2:2, STRUCT_0:def 5;
then x in {(1_ (gr {d}))} by X3, GROUP_2:def 7;
then x = 1_ (gr {d}) by TARSKI:def 1;
hence x = 1_ G by GROUP_2:44; :: thesis: verum
end;
hence ( x = 1_ G or gr {x} = gr {d} ) by GR_CY_1:12, A1, X1, X2; :: thesis: verum