let G be finite real-weighted WGraph; :: thesis: for i, j being Nat st i <= j holds
( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 )
let i, j be Nat; :: thesis: ( i <= j implies ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 ) )
set PCS = PRIM:CompSeq G;
set vPCS = ((PRIM:CompSeq G) . i) `1 ;
set ePCS = ((PRIM:CompSeq G) . i) `2 ;
assume i <= j ; :: thesis: ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 )
then consider x being Nat such that
A1: j = i + x by NAT_1:10;
defpred S₁[ Nat] means ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + $1)) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + $1)) `2 );
A3: S₁[ 0 ] ;

now

let k be Nat; :: thesis: ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + k)) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + k)) `2 implies ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + (k + 1))) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + (k + 1))) `2 ) )
assume A4: ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + k)) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + k)) `2 ) ; :: thesis: ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + (k + 1))) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + (k + 1))) `2 )
(PRIM:CompSeq G) . ((i + k) + 1) = PRIM:Step ((PRIM:CompSeq G) . (i + k)) by Def15;
then ( ((PRIM:CompSeq G) . (i + k)) `1 c= ((PRIM:CompSeq G) . ((i + k) + 1)) `1 & ((PRIM:CompSeq G) . (i + k)) `2 c= ((PRIM:CompSeq G) . ((i + k) + 1)) `2 ) by Lm7;
hence ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + (k + 1))) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + (k + 1))) `2 ) by A4, XBOOLE_1:1; :: thesis: verum

end;

then A5: for k being Nat st S₁[k] holds
S₁[k + 1] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A5);
hence ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 ) by A1; :: thesis: verum