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: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: 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
A3: m = (n + 1) + k by Th10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
n <= n + k by Th11;
then n c= n + k by A2;
then A4: succ n c= succ (n + k) by ORDINAL2:1;
(n + k) + 1 = succ (n + k) by Th39;
hence n + 1 c= m by A3, A4, Th39; :: thesis: verum

end;

assume A5: n + 1 c= m ; :: thesis: n + 1 <= m
n + 1 = succ n by Th39;
then A6: n in m by A5, ORDINAL1:21;
then n c= m by ORDINAL1:def 2;
then A7: n <= m by A2;
n <> m by A6;
then n < m by A7, XXREAL_0:1;
hence n + 1 <= m by Th13; :: thesis: verum

end;

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