defpred S1[ Nat, set , set ] means ( ( $2 is LexBFS:Labeling of G implies ex L being LexBFS:Labeling of G st
( $2 = L & $3 = LexBFS:Step L ) ) & ( $2 is not LexBFS:Labeling of G implies $3 = $2 ) );
now for n being Nat
for x being set ex y being set st S1[n,x,y]let n be
Nat;
for x being set ex y being set st S1[n,x,y]let x be
set ;
ex y being set st S1[n,x,y]now ex y being set st S1[n,x,y]end; hence
ex
y being
set st
S1[
n,
x,
y]
;
verum end;
then A1:
for n being Nat
for x being set ex y being set st S1[n,x,y]
;
consider IT being Function such that
A2:
( dom IT = NAT & IT . 0 = LexBFS:Init G & ( for n being Nat holds S1[n,IT . n,IT . (n + 1)] ) )
from RECDEF_1:sch 1(A1);
reconsider IT = IT as ManySortedSet of NAT by A2, PARTFUN1:def 2, RELAT_1:def 18;
defpred S2[ Nat] means IT . $1 is LexBFS:Labeling of G;
A3:
now for n being Nat st S2[n] holds
S2[n + 1]end;
A5:
S2[ 0 ]
by A2;
for n being Nat holds S2[n]
from NAT_1:sch 2(A5, A3);
then reconsider IT = IT as LexBFS:LabelingSeq of G by Def14;
take
IT
; ( IT . 0 = LexBFS:Init G & ( for n being Nat holds IT . (n + 1) = LexBFS:Step (IT . n) ) )
thus
IT . 0 = LexBFS:Init G
by A2; for n being Nat holds IT . (n + 1) = LexBFS:Step (IT . n)
let n be Nat; IT . (n + 1) = LexBFS:Step (IT . n)
ex Gn being LexBFS:Labeling of G st
( IT . n = Gn & IT . (n + 1) = LexBFS:Step Gn )
by A2;
hence
IT . (n + 1) = LexBFS:Step (IT . n)
; verum