let G be finite _Graph; :: thesis: ((LexBFS:CSeq G) .Result() ) `1 is with_property_T
set CS = LexBFS:CSeq G;
set L = ((LexBFS:CSeq G) .Result() ) `1 ;
A1: ((LexBFS:CSeq G) .Result() ) `1 is with_property_L3 by Th65;

now

let a, b, c be Vertex of G; :: thesis: ( a in dom (((LexBFS:CSeq G) .Result() ) `1 ) & b in dom (((LexBFS:CSeq G) .Result() ) `1 ) & c in dom (((LexBFS:CSeq G) .Result() ) `1 ) & (((LexBFS:CSeq G) .Result() ) `1 ) . a < (((LexBFS:CSeq G) .Result() ) `1 ) . b & (((LexBFS:CSeq G) .Result() ) `1 ) . b < (((LexBFS:CSeq G) .Result() ) `1 ) . c & a,c are_adjacent & not b,c are_adjacent implies ex d being Vertex of G st
( d in dom (((LexBFS:CSeq G) .Result() ) `1 ) & (((LexBFS:CSeq G) .Result() ) `1 ) . b < (((LexBFS:CSeq G) .Result() ) `1 ) . d & b,d are_adjacent & not a,d are_adjacent ) )
assume A2: ( a in dom (((LexBFS:CSeq G) .Result() ) `1 ) & b in dom (((LexBFS:CSeq G) .Result() ) `1 ) & c in dom (((LexBFS:CSeq G) .Result() ) `1 ) & (((LexBFS:CSeq G) .Result() ) `1 ) . a < (((LexBFS:CSeq G) .Result() ) `1 ) . b & (((LexBFS:CSeq G) .Result() ) `1 ) . b < (((LexBFS:CSeq G) .Result() ) `1 ) . c & a,c are_adjacent & not b,c are_adjacent ) ; :: thesis: ex d being Vertex of G st
( d in dom (((LexBFS:CSeq G) .Result() ) `1 ) & (((LexBFS:CSeq G) .Result() ) `1 ) . b < (((LexBFS:CSeq G) .Result() ) `1 ) . d & b,d are_adjacent & not a,d are_adjacent )
consider d being Vertex of G such that
A3: ( d in dom (((LexBFS:CSeq G) .Result() ) `1 ) & (((LexBFS:CSeq G) .Result() ) `1 ) . c < (((LexBFS:CSeq G) .Result() ) `1 ) . d & b,d are_adjacent & not a,d are_adjacent & ( for e being Vertex of G st e <> d & e,b are_adjacent & not e,a are_adjacent holds
(((LexBFS:CSeq G) .Result() ) `1 ) . e < (((LexBFS:CSeq G) .Result() ) `1 ) . d ) ) by A1, A2, Def34;
take d = d; :: thesis: ( d in dom (((LexBFS:CSeq G) .Result() ) `1 ) & (((LexBFS:CSeq G) .Result() ) `1 ) . b < (((LexBFS:CSeq G) .Result() ) `1 ) . d & b,d are_adjacent & not a,d are_adjacent )
thus d in dom (((LexBFS:CSeq G) .Result() ) `1 ) by A3; :: thesis: ( (((LexBFS:CSeq G) .Result() ) `1 ) . b < (((LexBFS:CSeq G) .Result() ) `1 ) . d & b,d are_adjacent & not a,d are_adjacent )
thus (((LexBFS:CSeq G) .Result() ) `1 ) . b < (((LexBFS:CSeq G) .Result() ) `1 ) . d by A2, A3, XXREAL_0:2; :: thesis: ( b,d are_adjacent & not a,d are_adjacent )
thus b,d are_adjacent by A3; :: thesis: not a,d are_adjacent
thus not a,d are_adjacent by A3; :: thesis: verum

end;

hence ((LexBFS:CSeq G) .Result() ) `1 is with_property_T by Def41; :: thesis: verum