defpred S₁[ Nat] means ( $1 * h = 0_ 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
( b₁ * h = 0_ G & b₁ <> 0 & ( for m being Nat st m * h = 0_ 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
( k * h = 0_ G & k <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
k <= m ) )
then A1: ex n being Nat st S₁[n] ;
consider k being Nat such that
A2: S₁[k] and
A3: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A1);
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k = k; :: thesis: ( k * h = 0_ G & k <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
k <= m ) )
thus ( k * h = 0_ G & k <> 0 ) by A2; :: thesis: for m being Nat st m * h = 0_ G & m <> 0 holds
k <= m
let m be Nat; :: thesis: ( m * h = 0_ G & m <> 0 implies k <= m )
assume ( m * h = 0_ G & m <> 0 ) ; :: thesis: k <= m
hence k <= m by A3; :: thesis: verum

end;