defpred S₁[ Nat] means ( x |^ $1 in BCK-part X & $1 <> 0 );
ex n being Element of NAT st
( n <> 0 & x |^ n in BCK-part X ) by A1;
then A2: ex n being Nat st S₁[n] ;
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 12;
take k ; :: thesis: ( x |^ k in BCK-part X & k <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
k <= m ) )
thus ( x |^ k in BCK-part X & k <> 0 ) by A3; :: thesis: for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
k <= m
let m be Element of NAT ; :: thesis: ( x |^ m in BCK-part X & m <> 0 implies k <= m )
assume ( x |^ m in BCK-part X & m <> 0 ) ; :: thesis: k <= m
hence k <= m by A4; :: thesis: verum