let m, n be Nat; :: thesis: ( n <= m iff Segm n c= Segm m )
defpred S₁[ Nat] means for m being Nat holds
( $1 <= m iff Segm $1 c= Segm 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 Segm (n + 1) c= Segm m )
thus ( n + 1 <= m implies Segm (n + 1) c= Segm m ) :: thesis: ( Segm (n + 1) c= Segm m implies n + 1 <= m )

proof

assume n + 1 <= m ; :: thesis: Segm (n + 1) c= Segm 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;
Segm n c= Segm (n + k) by A2, Th11;
then A4: succ (Segm n) c= succ (Segm (n + k)) by ORDINAL2:1;
Segm ((n + k) + 1) = succ (Segm (n + k)) by Th26;
hence Segm (n + 1) c= Segm m by A3, A4, Th26; :: thesis: verum

end;

assume A5: Segm (n + 1) c= Segm m ; :: thesis: n + 1 <= m
Segm (n + 1) = succ (Segm n) by Th26;
then A6: n in Segm m by A5, ORDINAL1:21;
then A7: n <= m by A2, ORDINAL1:def 2;
reconsider nn = n as set ;
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 Segm n c= Segm m ) ; :: thesis: verum