let m, n be Nat; :: thesis: ( n <= m iff Segm n c= Segm m )
defpred S1[ Nat] means for m being Nat holds
( $1 <= m iff Segm $1 c= Segm m );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[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: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A8, A1);
 hence ( n <= m iff Segm n c= Segm m ) ; :: thesis: verum