let G be _finite real-weighted WGraph; :: thesis: for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G
set src = the Element of the_Vertices_of G;
defpred S<sub>1</sub>[ Nat] means ((PRIM:CompSeq G) . $1) `1 c= G .reachableFrom the Element of the_Vertices_of G;
set G0 = (PRIM:CompSeq G) . 0;
(PRIM:CompSeq G) . 0 = PRIM:Init G by Def17;
then A1: ((PRIM:CompSeq G) . 0) `1 = { the Element of the_Vertices_of G} ;

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
set Gn = (PRIM:CompSeq G) . n;
set Gn1 = (PRIM:CompSeq G) . (n + 1);
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set e = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set sc = (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set tar = (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
A4: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def17;

now :: thesis: S₁[n + 1]

per cases ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} or ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) or ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & not (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ) ;

suppose PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: S₁[n + 1]

hence S₁[n + 1] by A3, A4, Def15; :: thesis: verum

end;

suppose A5: ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ; :: thesis: S₁[n + 1]

then (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))}),((((PRIM:CompSeq G) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)})] by A4, Def15;
then A6: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ;
A7: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by A5;

now :: thesis: for v being object st v in ((PRIM:CompSeq G) . (n + 1)) `1 holds
v in G .reachableFrom the Element of the_Vertices_of G

let v be object ; :: thesis: ( v in ((PRIM:CompSeq G) . (n + 1)) `1 implies v in G .reachableFrom the Element of the_Vertices_of G )
assume A8: v in ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: v in G .reachableFrom the Element of the_Vertices_of G

now :: thesis: v in G .reachableFrom the Element of the_Vertices_of G

per cases ( v in ((PRIM:CompSeq G) . n) `1 or v in {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ) by A6, A8, XBOOLE_0:def 3;

suppose v in ((PRIM:CompSeq G) . n) `1 ; :: thesis: v in G .reachableFrom the Element of the_Vertices_of G

hence v in G .reachableFrom the Element of the_Vertices_of G by A3; :: thesis: verum

end;

suppose v in {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ; :: thesis: v in G .reachableFrom the Element of the_Vertices_of G

then v = (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by TARSKI:def 1;
then the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) Joins (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n),v,G by A7;
hence v in G .reachableFrom the Element of the_Vertices_of G by A3, A5, GLIB_002:10; :: thesis: verum

end;

end;

end;

hence v in G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum

end;

hence S₁[n + 1] by TARSKI:def 3; :: thesis: verum

end;

suppose A9: ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & not (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ; :: thesis: S₁[n + 1]

then (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))}),((((PRIM:CompSeq G) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)})] by A4, Def15;
then A10: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ;
A11: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G by A9, Def13;
then A12: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in the_Edges_of G ;
A13: (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 by A9, A11;

now :: thesis: for v being object st v in ((PRIM:CompSeq G) . (n + 1)) `1 holds
v in G .reachableFrom the Element of the_Vertices_of G

let v be object ; :: thesis: ( v in ((PRIM:CompSeq G) . (n + 1)) `1 implies v in G .reachableFrom the Element of the_Vertices_of G )
assume A14: v in ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: v in G .reachableFrom the Element of the_Vertices_of G

now :: thesis: v in G .reachableFrom the Element of the_Vertices_of G

per cases ( v in ((PRIM:CompSeq G) . n) `1 or v in {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ) by A10, A14, XBOOLE_0:def 3;

suppose v in ((PRIM:CompSeq G) . n) `1 ; :: thesis: v in G .reachableFrom the Element of the_Vertices_of G

hence v in G .reachableFrom the Element of the_Vertices_of G by A3; :: thesis: verum

end;

suppose v in {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ; :: thesis: v in G .reachableFrom the Element of the_Vertices_of G

then v = (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by TARSKI:def 1;
then the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) Joins (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n),v,G by A12;
hence v in G .reachableFrom the Element of the_Vertices_of G by A3, A13, GLIB_002:10; :: thesis: verum

end;

end;

end;

hence v in G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum

end;

hence S₁[n + 1] by TARSKI:def 3; :: thesis: verum

end;

end;

end;

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

end;

the Element of the_Vertices_of G in G .reachableFrom the Element of the_Vertices_of G by GLIB_002:9;
then A15: S₁[ 0 ] by A1, ZFMISC_1:31;
for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A2);
hence for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum