set FAP = AP:FindAugPath EL,source;
set CS = AP:CompSeq EL,source;
let IT1, IT2 be vertex-distinct Path of G; :: thesis:
defpred S₁[ Nat] means for v being set
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq EL,source) . $1) & P1 is_Walk_from source,v & P1 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 is_augmenting_wrt EL & ( for n being even Nat st n in dom P1 holds
P1 . n = (AP:FindAugPath EL,source) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath EL,source) . (P2 . (n + 1)) ) holds
P1 = P2;
set G0 = (AP:CompSeq EL,source) . 0 ;

now

let n be Nat; :: thesis:
assume A87: S₁[n] ; :: thesis:
set Gn = (AP:CompSeq EL,source) . n;
set Gn1 = (AP:CompSeq EL,source) . (n + 1);
set Next = AP:NextBestEdges ((AP:CompSeq EL,source) . n);
set e = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n));
A88: (AP:CompSeq EL,source) . (n + 1) = AP:Step ((AP:CompSeq EL,source) . n) by Def12;

now

per cases ;

suppose AP:NextBestEdges ((AP:CompSeq EL,source) . n) = {} ; :: thesis:

then (AP:CompSeq EL,source) . (n + 1) = (AP:CompSeq EL,source) . n by A88, Def10;
hence S₁[n + 1] by A87; :: thesis:

end;

suppose A89: ( AP:NextBestEdges ((AP:CompSeq EL,source) . n) <> {} & not (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) ) ; :: thesis:

now

let v be set ; :: thesis:
let P1, P2 be vertex-distinct Path of G; :: thesis:
assume that
A95: v in dom ((AP:CompSeq EL,source) . (n + 1)) and
A96: P1 is_Walk_from source,v and
A97: P1 is_augmenting_wrt EL and
A98: P2 is_Walk_from source,v and
A99: P2 is_augmenting_wrt EL and
A100: for n being even Nat st n in dom P1 holds
P1 . n = (AP:FindAugPath EL,source) . (P1 . (n + 1)) and
A101: for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath EL,source) . (P2 . (n + 1)) ; :: thesis:
A102: P1 . (len P1) = v by A96, GLIB_001:18;
A103: P2 . 1 = source by A98, GLIB_001:18;
A104: P2 . (len P2) = v by A98, GLIB_001:18;
A105: P1 . 1 = source by A96, GLIB_001:18;

now

per cases by A94, A95, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq EL,source) . n) ; :: thesis:

hence P1 = P2 by A87, A96, A97, A98, A99, A100, A101; :: thesis:

end;

suppose A106: v in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ; :: thesis:

then A107: v = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by TARSKI:def 1;
then ((AP:CompSeq EL,source) . (n + 1)) . v = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) by A93, Lm3;
then A108: (AP:FindAugPath EL,source) . v = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) by A95, Th7;
A109: v <> source by A89, A91, A106, TARSKI:def 1;
then P1 . 1 <> P1 .last() by A105, A102, GLIB_001:def 7;
then P1 .first() <> P1 .last() by GLIB_001:def 6;
then not P1 is trivial by GLIB_001:128;
then A110: 3 <= len P1 by GLIB_001:126;
P2 . 1 <> P2 .last() by A103, A104, A109, GLIB_001:def 7;
then P2 .first() <> P2 .last() by GLIB_001:def 6;
then not P2 is trivial by GLIB_001:128;
then A111: 3 <= len P2 by GLIB_001:126;
then A112: 3 - 2 < (len P2) - 0 by XREAL_1:17;
3 - 2 < (len P1) - 0 by A110, XREAL_1:17;
then reconsider lenP11 = (len P1) - 1, lenP21 = (len P2) - 1 as even Element of NAT by A112, INT_1:18;
A113: lenP11 < (len P1) - 0 by XREAL_1:17;
3 - 2 <= lenP11 by A110, XREAL_1:17;
then A114: lenP11 in dom P1 by A113, FINSEQ_3:27;
lenP11 + 1 = len P1 ;
then A115: P1 . lenP11 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) by A100, A102, A114, A108;
then consider lenP12 being odd Element of NAT such that
A116: lenP12 = lenP11 - 1 and
lenP11 - 1 in dom P1 and
lenP11 + 1 in dom P1 and
A117: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins P1 . lenP12,v,G by A102, A114, GLIB_001:10;
A118: P1 . lenP12 = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by A89, A92, A107, A117, GLIB_000:def 15;
set P1A = P1 .cut ((2 * 0 ) + 1),lenP12;
A119: lenP12 < len P1 by A113, A116, XREAL_1:17;

A120: now

let n be even Nat; :: thesis:
assume A121: n in dom (P1 .cut ((2 * 0 ) + 1),lenP12) ; :: thesis:
then A122: 1 <= n by FINSEQ_3:27;
A123: n <= len (P1 .cut ((2 * 0 ) + 1),lenP12) by A121, FINSEQ_3:27;
then n < len (P1 .cut ((2 * 0 ) + 1),lenP12) by XXREAL_0:1;
then A124: n + 1 <= len (P1 .cut ((2 * 0 ) + 1),lenP12) by NAT_1:13;
1 <= n + 1 by A121, NAT_1:13;
then n + 1 in dom (P1 .cut ((2 * 0 ) + 1),lenP12) by A124, FINSEQ_3:27;
then A125: (P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1) = P1 . (n + 1) by A119, GLIB_001:47;
len (P1 .cut ((2 * 0 ) + 1),lenP12) = lenP12 by A119, GLIB_001:46;
then n <= len P1 by A119, A123, XXREAL_0:2;
then A126: n in dom P1 by A122, FINSEQ_3:27;
(P1 .cut ((2 * 0 ) + 1),lenP12) . n = P1 . n by A119, A121, GLIB_001:47;
hence (P1 .cut ((2 * 0 ) + 1),lenP12) . n = (AP:FindAugPath EL,source) . ((P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1)) by A100, A125, A126; :: thesis:

end;

A127: lenP12 + (1 + 1) = len P1 by A116;
lenP12 + 1 = lenP11 by A116;
then A128: P1 .cut lenP12,(len P1) = G .walkOf ((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),v by A102, A115, A118, A119, A127, GLIB_001:41;
A129: P1 .cut ((2 * 0 ) + 1),lenP12 is_augmenting_wrt EL by A97, Th2;
A130: 1 <= lenP12 by HEYTING3:1;
then A131: (P1 .cut ((2 * 0 ) + 1),lenP12) .append (P1 .cut lenP12,(len P1)) = P1 .cut ((2 * 0 ) + 1),(len P1) by A119, GLIB_001:39
.= P1 by GLIB_001:40 ;
A132: lenP21 < (len P2) - 0 by XREAL_1:17;
3 - 2 <= lenP21 by A111, XREAL_1:17;
then A133: lenP21 in dom P2 by A132, FINSEQ_3:27;
lenP21 + 1 = len P2 ;
then A134: P2 . lenP21 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) by A101, A104, A133, A108;
then consider lenP22 being odd Element of NAT such that
A135: lenP22 = lenP21 - 1 and
lenP21 - 1 in dom P2 and
lenP21 + 1 in dom P2 and
A136: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins P2 . lenP22,v,G by A104, A133, GLIB_001:10;
A137: lenP22 + (1 + 1) = len P2 by A135;
set P2A = P2 .cut ((2 * 0 ) + 1),lenP22;
A138: lenP22 < len P2 by A132, A135, XREAL_1:17;

A139: now

let n be even Nat; :: thesis:
assume A140: n in dom (P2 .cut ((2 * 0 ) + 1),lenP22) ; :: thesis:
then A141: 1 <= n by FINSEQ_3:27;
A142: n <= len (P2 .cut ((2 * 0 ) + 1),lenP22) by A140, FINSEQ_3:27;
then n < len (P2 .cut ((2 * 0 ) + 1),lenP22) by XXREAL_0:1;
then A143: n + 1 <= len (P2 .cut ((2 * 0 ) + 1),lenP22) by NAT_1:13;
1 <= n + 1 by A140, NAT_1:13;
then n + 1 in dom (P2 .cut ((2 * 0 ) + 1),lenP22) by A143, FINSEQ_3:27;
then A144: (P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1) = P2 . (n + 1) by A138, GLIB_001:47;
len (P2 .cut ((2 * 0 ) + 1),lenP22) = lenP22 by A138, GLIB_001:46;
then n <= len P2 by A138, A142, XXREAL_0:2;
then A145: n in dom P2 by A141, FINSEQ_3:27;
(P2 .cut ((2 * 0 ) + 1),lenP22) . n = P2 . n by A138, A140, GLIB_001:47;
hence (P2 .cut ((2 * 0 ) + 1),lenP22) . n = (AP:FindAugPath EL,source) . ((P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1)) by A101, A144, A145; :: thesis:

end;

A146: 1 <= lenP22 by HEYTING3:1;
then A147: (P2 .cut ((2 * 0 ) + 1),lenP22) .append (P2 .cut lenP22,(len P2)) = P2 .cut ((2 * 0 ) + 1),(len P2) by A138, GLIB_001:39
.= P2 by GLIB_001:40 ;
A148: P2 . lenP22 = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by A89, A92, A107, A136, GLIB_000:def 15;
then A149: P2 .cut ((2 * 0 ) + 1),lenP22 is_Walk_from source,(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by A103, A146, A138, GLIB_001:38;
lenP22 + 1 = lenP21 by A135;
then A150: P2 .cut lenP22,(len P2) = G .walkOf ((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),v by A104, A134, A148, A138, A137, GLIB_001:41;
A151: P2 .cut ((2 * 0 ) + 1),lenP22 is_augmenting_wrt EL by A99, Th2;
P1 .cut ((2 * 0 ) + 1),lenP12 is_Walk_from source,(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by A105, A118, A130, A119, GLIB_001:38;
hence P1 = P2 by A87, A92, A149, A129, A151, A120, A139, A128, A150, A131, A147; :: thesis:

end;

hence P1 = P2 ; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

suppose A152: ( AP:NextBestEdges ((AP:CompSeq EL,source) . n) <> {} & (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) ) ; :: thesis:

now

let v be set ; :: thesis:
let P1, P2 be vertex-distinct Path of G; :: thesis:
assume that
A158: v in dom ((AP:CompSeq EL,source) . (n + 1)) and
A159: P1 is_Walk_from source,v and
A160: P1 is_augmenting_wrt EL and
A161: P2 is_Walk_from source,v and
A162: P2 is_augmenting_wrt EL and
A163: for n being even Nat st n in dom P1 holds
P1 . n = (AP:FindAugPath EL,source) . (P1 . (n + 1)) and
A164: for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath EL,source) . (P2 . (n + 1)) ; :: thesis:
A165: P1 . (len P1) = v by A159, GLIB_001:18;
A166: P2 . 1 = source by A161, GLIB_001:18;
A167: P2 . (len P2) = v by A161, GLIB_001:18;
A168: P1 . 1 = source by A159, GLIB_001:18;

now

per cases by A157, A158, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq EL,source) . n) ; :: thesis:

hence P1 = P2 by A87, A159, A160, A161, A162, A163, A164; :: thesis:

end;

suppose A169: v in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ; :: thesis:

then A170: v = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by TARSKI:def 1;
then ((AP:CompSeq EL,source) . (n + 1)) . v = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) by A156, Lm3;
then A171: (AP:FindAugPath EL,source) . v = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) by A158, Th7;
A172: v <> source by A155, A154, A169, TARSKI:def 1;
then P1 . 1 <> P1 .last() by A168, A165, GLIB_001:def 7;
then P1 .first() <> P1 .last() by GLIB_001:def 6;
then not P1 is trivial by GLIB_001:128;
then A173: 3 <= len P1 by GLIB_001:126;
P2 . 1 <> P2 .last() by A166, A167, A172, GLIB_001:def 7;
then P2 .first() <> P2 .last() by GLIB_001:def 6;
then not P2 is trivial by GLIB_001:128;
then A174: 3 <= len P2 by GLIB_001:126;
then A175: 3 - 2 < (len P2) - 0 by XREAL_1:17;
3 - 2 < (len P1) - 0 by A173, XREAL_1:17;
then reconsider lenP11 = (len P1) - 1, lenP21 = (len P2) - 1 as even Element of NAT by A175, INT_1:18;
A176: lenP11 < (len P1) - 0 by XREAL_1:17;
3 - 2 <= lenP11 by A173, XREAL_1:17;
then A177: lenP11 in dom P1 by A176, FINSEQ_3:27;
lenP11 + 1 = len P1 ;
then A178: P1 . lenP11 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) by A163, A165, A177, A171;
then consider lenP12 being odd Element of NAT such that
A179: lenP12 = lenP11 - 1 and
lenP11 - 1 in dom P1 and
lenP11 + 1 in dom P1 and
A180: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins P1 . lenP12,v,G by A165, A177, GLIB_001:10;
A181: P1 . lenP12 = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by A152, A155, A170, A180, GLIB_000:def 15;
set P1A = P1 .cut ((2 * 0 ) + 1),lenP12;
A182: lenP12 < len P1 by A176, A179, XREAL_1:17;

A183: now

let n be even Nat; :: thesis:
assume A184: n in dom (P1 .cut ((2 * 0 ) + 1),lenP12) ; :: thesis:
then A185: 1 <= n by FINSEQ_3:27;
A186: n <= len (P1 .cut ((2 * 0 ) + 1),lenP12) by A184, FINSEQ_3:27;
then n < len (P1 .cut ((2 * 0 ) + 1),lenP12) by XXREAL_0:1;
then A187: n + 1 <= len (P1 .cut ((2 * 0 ) + 1),lenP12) by NAT_1:13;
1 <= n + 1 by A184, NAT_1:13;
then n + 1 in dom (P1 .cut ((2 * 0 ) + 1),lenP12) by A187, FINSEQ_3:27;
then A188: (P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1) = P1 . (n + 1) by A182, GLIB_001:47;
len (P1 .cut ((2 * 0 ) + 1),lenP12) = lenP12 by A182, GLIB_001:46;
then n <= len P1 by A182, A186, XXREAL_0:2;
then A189: n in dom P1 by A185, FINSEQ_3:27;
(P1 .cut ((2 * 0 ) + 1),lenP12) . n = P1 . n by A182, A184, GLIB_001:47;
hence (P1 .cut ((2 * 0 ) + 1),lenP12) . n = (AP:FindAugPath EL,source) . ((P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1)) by A163, A188, A189; :: thesis:

end;

A190: lenP12 + (1 + 1) = len P1 by A179;
lenP12 + 1 = lenP11 by A179;
then A191: P1 .cut lenP12,(len P1) = G .walkOf ((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),v by A165, A178, A181, A182, A190, GLIB_001:41;
A192: P1 .cut ((2 * 0 ) + 1),lenP12 is_augmenting_wrt EL by A160, Th2;
A193: 1 <= lenP12 by HEYTING3:1;
then A194: (P1 .cut ((2 * 0 ) + 1),lenP12) .append (P1 .cut lenP12,(len P1)) = P1 .cut ((2 * 0 ) + 1),(len P1) by A182, GLIB_001:39
.= P1 by GLIB_001:40 ;
A195: lenP21 < (len P2) - 0 by XREAL_1:17;
3 - 2 <= lenP21 by A174, XREAL_1:17;
then A196: lenP21 in dom P2 by A195, FINSEQ_3:27;
lenP21 + 1 = len P2 ;
then A197: P2 . lenP21 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) by A164, A167, A196, A171;
then consider lenP22 being odd Element of NAT such that
A198: lenP22 = lenP21 - 1 and
lenP21 - 1 in dom P2 and
lenP21 + 1 in dom P2 and
A199: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins P2 . lenP22,v,G by A167, A196, GLIB_001:10;
A200: lenP22 + (1 + 1) = len P2 by A198;
set P2A = P2 .cut ((2 * 0 ) + 1),lenP22;
A201: lenP22 < len P2 by A195, A198, XREAL_1:17;

A202: now

let n be even Nat; :: thesis:
assume A203: n in dom (P2 .cut ((2 * 0 ) + 1),lenP22) ; :: thesis:
then A204: 1 <= n by FINSEQ_3:27;
A205: n <= len (P2 .cut ((2 * 0 ) + 1),lenP22) by A203, FINSEQ_3:27;
then n < len (P2 .cut ((2 * 0 ) + 1),lenP22) by XXREAL_0:1;
then A206: n + 1 <= len (P2 .cut ((2 * 0 ) + 1),lenP22) by NAT_1:13;
1 <= n + 1 by A203, NAT_1:13;
then n + 1 in dom (P2 .cut ((2 * 0 ) + 1),lenP22) by A206, FINSEQ_3:27;
then A207: (P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1) = P2 . (n + 1) by A201, GLIB_001:47;
len (P2 .cut ((2 * 0 ) + 1),lenP22) = lenP22 by A201, GLIB_001:46;
then n <= len P2 by A201, A205, XXREAL_0:2;
then A208: n in dom P2 by A204, FINSEQ_3:27;
(P2 .cut ((2 * 0 ) + 1),lenP22) . n = P2 . n by A201, A203, GLIB_001:47;
hence (P2 .cut ((2 * 0 ) + 1),lenP22) . n = (AP:FindAugPath EL,source) . ((P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1)) by A164, A207, A208; :: thesis:

end;

A209: 1 <= lenP22 by HEYTING3:1;
then A210: (P2 .cut ((2 * 0 ) + 1),lenP22) .append (P2 .cut lenP22,(len P2)) = P2 .cut ((2 * 0 ) + 1),(len P2) by A201, GLIB_001:39
.= P2 by GLIB_001:40 ;
A211: P2 . lenP22 = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by A152, A155, A170, A199, GLIB_000:def 15;
then A212: P2 .cut ((2 * 0 ) + 1),lenP22 is_Walk_from source,(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by A166, A209, A201, GLIB_001:38;
lenP22 + 1 = lenP21 by A198;
then A213: P2 .cut lenP22,(len P2) = G .walkOf ((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),v by A167, A197, A211, A201, A200, GLIB_001:41;
A214: P2 .cut ((2 * 0 ) + 1),lenP22 is_augmenting_wrt EL by A162, Th2;
P1 .cut ((2 * 0 ) + 1),lenP12 is_Walk_from source,(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by A168, A181, A193, A182, GLIB_001:38;
hence P1 = P2 by A87, A152, A212, A192, A214, A183, A202, A191, A213, A194, A210; :: thesis:

end;

hence P1 = P2 ; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

then A215: for n being Nat st S₁[n] holds
S₁[n + 1] ;

now

let v be set ; :: thesis:
let P1, P2 be vertex-distinct Path of G; :: thesis:
assume that
A216: v in dom ((AP:CompSeq EL,source) . 0 ) and
A217: P1 is_Walk_from source,v and
P1 is_augmenting_wrt EL and
A218: P2 is_Walk_from source,v and
P2 is_augmenting_wrt EL and
for n being even Nat st n in dom P1 holds
P1 . n = (AP:FindAugPath EL,source) . (P1 . (n + 1)) and
for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath EL,source) . (P2 . (n + 1)) ; :: thesis:
v in {source} by A216, Th4;
then A219: v = source by TARSKI:def 1;
then A220: P1 . ((2 * 0 ) + 1) = v by A217, GLIB_001:18;
A221: P2 . ((2 * 0 ) + 1) = v by A218, A219, GLIB_001:18;
A222: 1 <= len P1 by HEYTING3:1;
P1 . (len P1) = v by A217, GLIB_001:18;
then len P1 = 1 by A220, A222, GLIB_001:def 29;
then A223: P1 = <*v*> by A220, FINSEQ_1:57;
A224: 1 <= len P2 by HEYTING3:1;
P2 . (len P2) = v by A218, GLIB_001:18;
then len P2 = 1 by A221, A224, GLIB_001:def 29;
hence P1 = P2 by A221, A223, FINSEQ_1:57; :: thesis:

end;

then A225: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A225, A215);
hence ( sink in dom (AP:FindAugPath EL,source) & IT1 is_Walk_from source,sink & IT1 is_augmenting_wrt EL & ( for n being even Nat st n in dom IT1 holds
IT1 . n = (AP:FindAugPath EL,source) . (IT1 . (n + 1)) ) & IT2 is_Walk_from source,sink & IT2 is_augmenting_wrt EL & ( for n being even Nat st n in dom IT2 holds
IT2 . n = (AP:FindAugPath EL,source) . (IT2 . (n + 1)) ) implies IT1 = IT2 ) ; :: thesis:
thus ( not sink in dom (AP:FindAugPath EL,source) & IT1 = G .walkOf source & IT2 = G .walkOf source implies IT1 = IT2 ) ; :: thesis: