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 Th53;

now :: thesis: for a, b, c being Vertex of G st 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 holds
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 )

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 that
A2: a in dom (((LexBFS:CSeq G) .Result()) `1) and
A3: b in dom (((LexBFS:CSeq G) .Result()) `1) and
A4: c in dom (((LexBFS:CSeq G) .Result()) `1) and
A5: (((LexBFS:CSeq G) .Result()) `1) . a < (((LexBFS:CSeq G) .Result()) `1) . b and
A6: (((LexBFS:CSeq G) .Result()) `1) . b < (((LexBFS:CSeq G) .Result()) `1) . c and
A7: a,c are_adjacent and
A8: 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
A9: d in dom (((LexBFS:CSeq G) .Result()) `1) and
A10: (((LexBFS:CSeq G) .Result()) `1) . c < (((LexBFS:CSeq G) .Result()) `1) . d and
A11: b,d are_adjacent and
A12: not a,d are_adjacent and
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, A3, A4, A5, A6, A7, A8;
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 A9; :: 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 A6, A10, XXREAL_0:2; :: thesis: ( b,d are_adjacent & not a,d are_adjacent )
thus b,d are_adjacent by A11; :: thesis: not a,d are_adjacent
thus not a,d are_adjacent by A12; :: thesis: verum

end;

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