let G be _finite real-weighted WGraph; :: thesis: for n being Nat holds
( ((PRIM:CompSeq G) . n) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . n) `2 c= G .edgesBetween (((PRIM:CompSeq G) . n) `1) )
set PCS = PRIM:CompSeq G;
defpred S<sub>1</sub>[ Nat] means ( ((PRIM:CompSeq G) . $1) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . $1) `2 c= G .edgesBetween (((PRIM:CompSeq G) . $1) `1) );
A1: ((PRIM:CompSeq G) . 0) `2 = (PRIM:Init G) `2 by Def17
.= {} ;

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 A2: 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);
A3: (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) <> {} ) ;

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

then (PRIM:CompSeq G) . (n + 1) = (PRIM:CompSeq G) . n by A3, Def15;
hence S₁[n + 1] by A2; :: thesis: verum

end;

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

set src = (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);
A5: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by A4;
A6: 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 A4, Def13;

now :: thesis: ( ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) )

per cases ( (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 or not (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ;

suppose A7: (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ; :: thesis: ( ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) )

then A8: (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 A3, A4, Def15;
then A9: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ;
then A10: G .edgesBetween (((PRIM:CompSeq G) . n) `1) c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by GLIB_000:36, XBOOLE_1:7;
thus ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) by A8; :: thesis: ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)
A11: ((PRIM:CompSeq G) . (n + 1)) `2 = (((PRIM:CompSeq G) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)} by A8;
A12: ((PRIM:CompSeq G) . n) `1 c= ((PRIM:CompSeq G) . (n + 1)) `1 by A9, XBOOLE_1:7;

now :: thesis: for x being object st x in ((PRIM:CompSeq G) . (n + 1)) `2 holds
x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

let x be object ; :: thesis: ( x in ((PRIM:CompSeq G) . (n + 1)) `2 implies x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) )
assume A13: x in ((PRIM:CompSeq G) . (n + 1)) `2 ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

now :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

per cases ( x in ((PRIM:CompSeq G) . n) `2 or x in { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)} ) by A11, A13, XBOOLE_0:def 3;

suppose x in ((PRIM:CompSeq G) . n) `2 ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

then x in G .edgesBetween (((PRIM:CompSeq G) . n) `1) by A2;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by A10; :: thesis: verum

end;

suppose x in { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)} ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

then A14: x = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by TARSKI:def 1;
then (the_Target_of G) . x in {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} by TARSKI:def 1;
then (the_Target_of G) . x in ((PRIM:CompSeq G) . (n + 1)) `1 by A9, XBOOLE_0:def 3;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by A5, A7, A12, A14, GLIB_000:31; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) ; :: thesis: verum

end;

hence ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) ; :: thesis: verum

end;

suppose A15: not (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ; :: thesis: ( ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) )

then A16: (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 by A6;
A17: (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 A3, A4, A15, Def15;
then A18: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ;
then A19: G .edgesBetween (((PRIM:CompSeq G) . n) `1) c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by GLIB_000:36, XBOOLE_1:7;
thus ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) by A17; :: thesis: ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)
A20: ((PRIM:CompSeq G) . (n + 1)) `2 = (((PRIM:CompSeq G) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)} by A17;
A21: ((PRIM:CompSeq G) . n) `1 c= ((PRIM:CompSeq G) . (n + 1)) `1 by A18, XBOOLE_1:7;

now :: thesis: for x being object st x in ((PRIM:CompSeq G) . (n + 1)) `2 holds
x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

let x be object ; :: thesis: ( x in ((PRIM:CompSeq G) . (n + 1)) `2 implies x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) )
assume A22: x in ((PRIM:CompSeq G) . (n + 1)) `2 ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

now :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

per cases ( x in ((PRIM:CompSeq G) . n) `2 or x in { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)} ) by A20, A22, XBOOLE_0:def 3;

suppose x in ((PRIM:CompSeq G) . n) `2 ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

then x in G .edgesBetween (((PRIM:CompSeq G) . n) `1) by A2;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by A19; :: thesis: verum

end;

suppose x in { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)} ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)

then A23: x = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by TARSKI:def 1;
then (the_Source_of G) . x in {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} by TARSKI:def 1;
then (the_Source_of G) . x in ((PRIM:CompSeq G) . (n + 1)) `1 by A18, XBOOLE_0:def 3;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by A5, A21, A16, A23, GLIB_000:31; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) ; :: thesis: verum

end;

hence ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

then A24: for n being Nat st S₁[n] holds
S₁[n + 1] ;
((PRIM:CompSeq G) . 0) `1 = (PRIM:Init G) `1 by Def17
.= { the Element of the_Vertices_of G} ;
then A25: S₁[ 0 ] by A1, XBOOLE_1:2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A25, A24);
hence for n being Nat holds
( ((PRIM:CompSeq G) . n) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . n) `2 c= G .edgesBetween (((PRIM:CompSeq G) . n) `1) ) ; :: thesis: verum