defpred S_{1}[ 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 ) );

for x being set ex y being set st S_{1}[n,x,y]
;

consider IT being Function such that

A2: ( dom IT = NAT & IT . 0 = LexBFS:Init G & ( for n being Nat holds S_{1}[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 S_{2}[ Nat] means IT . $1 is LexBFS:Labeling of G;

_{2}[ 0 ]
by A2;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A5, A3);

then reconsider IT = IT as LexBFS:LabelingSeq of G by Def14;

take IT ; :: thesis: ( 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; :: thesis: for n being Nat holds IT . (n + 1) = LexBFS:Step (IT . n)

let n be Nat; :: thesis: 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) ; :: thesis: verum

( $2 = L & $3 = LexBFS:Step L ) ) & ( $2 is not LexBFS:Labeling of G implies $3 = $2 ) );

now :: thesis: for n being Nat

for x being set ex y being set st S_{1}[n,x,y]

then A1:
for n being Natfor x being set ex y being set st S

let n be Nat; :: thesis: for x being set ex y being set st S_{1}[n,x,y]

let x be set ; :: thesis: ex y being set st S_{1}[n,x,y]

_{1}[n,x,y]
; :: thesis: verum

end;let x be set ; :: thesis: ex y being set st S

now :: thesis: ex y being set st S_{1}[n,x,y]end;

hence
ex y being set st Sper cases
( x is LexBFS:Labeling of G or not x is LexBFS:Labeling of G )
;

end;

suppose
x is LexBFS:Labeling of G
; :: thesis: ex y being set st S_{1}[n,x,y]

then reconsider L = x as LexBFS:Labeling of G ;

LexBFS:Step L = LexBFS:Step L ;

hence ex y being set st S_{1}[n,x,y]
; :: thesis: verum

end;LexBFS:Step L = LexBFS:Step L ;

hence ex y being set st S

for x being set ex y being set st S

consider IT being Function such that

A2: ( dom IT = NAT & IT . 0 = LexBFS:Init G & ( for n being Nat holds S

reconsider IT = IT as ManySortedSet of NAT by A2, PARTFUN1:def 2, RELAT_1:def 18;

defpred S

A3: now :: thesis: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

A5:
SS

let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A4: S_{2}[n]
; :: thesis: S_{2}[n + 1]

ex Gn being LexBFS:Labeling of G st

( IT . n = Gn & IT . (n + 1) = LexBFS:Step Gn ) by A2, A4;

hence S_{2}[n + 1]
; :: thesis: verum

end;assume A4: S

ex Gn being LexBFS:Labeling of G st

( IT . n = Gn & IT . (n + 1) = LexBFS:Step Gn ) by A2, A4;

hence S

for n being Nat holds S

then reconsider IT = IT as LexBFS:LabelingSeq of G by Def14;

take IT ; :: thesis: ( 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; :: thesis: for n being Nat holds IT . (n + 1) = LexBFS:Step (IT . n)

let n be Nat; :: thesis: 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) ; :: thesis: verum