let n, m be Nat; :: thesis: ( n <= m iff n c= m )
defpred S₁[ Nat] means for m being Nat holds
( $1 <= m iff $1 c= m );
A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let m be Nat; :: thesis: ( n + 1 <= m iff n + 1 c= m )
thus ( n + 1 <= m implies n + 1 c= m ) :: thesis: ( n + 1 c= m implies n + 1 <= m )

proof

assume n + 1 <= m ; :: thesis: n + 1 c= m
then consider k being Nat such that
A4: m = (n + 1) + k by Th10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
n <= n + k by Th11;
then n c= n + k by A3;
then ( succ n c= succ (n + k) & n + 1 = succ n & (n + k) + 1 = succ (n + k) ) by Th39, ORDINAL2:1;
hence n + 1 c= m by A4; :: thesis: verum

end;

assume A5: n + 1 c= m ; :: thesis: n + 1 <= m
n + 1 = succ n by Th39;
then n in m by A5, ORDINAL1:33;
then ( n c= m & n <> m ) by ORDINAL1:def 2;
then ( n <= m & n <> m ) by A3;
then n < m by XXREAL_0:1;
hence n + 1 <= m by Th13; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence ( n <= m iff n c= m ) ; :: thesis: verum