defpred S₁[ Nat] means ( h |^ $1 = 1_ G & $1 <> 0 );
thus ( h is being_of_order_0 implies ex n being Element of NAT st n = 0 ) ; :: thesis: ( not h is being_of_order_0 implies ex b₁ being Element of NAT st
( h |^ b₁ = 1_ G & b₁ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₁ <= m ) ) )

hereby :: thesis: verum

assume not h is being_of_order_0 ; :: thesis: ex k being Element of NAT st
( h |^ k = 1_ G & k <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m ) )
then consider n being Nat such that
A1: ( h |^ n = 1_ G & n <> 0 ) by Def11;
A2: ex n being Nat st S₁[n] by A1;
consider k being Nat such that
A3: S₁[k] and
A4: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A2);
reconsider k = k as Element of NAT by ORDINAL1:def 13;
take k = k; :: thesis: ( h |^ k = 1_ G & k <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m ) )
thus ( h |^ k = 1_ G & k <> 0 ) by A3; :: thesis: for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m
let m be Nat; :: thesis: ( h |^ m = 1_ G & m <> 0 implies k <= m )
assume ( h |^ m = 1_ G & m <> 0 ) ; :: thesis: k <= m
hence k <= m by A4; :: thesis: verum

end;