:: deftheorem defines with_property_T LEXBFS:def 27 :
for G being _Graph
for F being PartFunc of (the_Vertices_of G),NAT holds
( F is with_property_T iff for a, b, c being Vertex of G st a in dom F & b in dom F & c in dom F & F . a < F . b & F . b < F . c & a,c are_adjacent & not b,c are_adjacent holds
ex d being Vertex of G st
( d in dom F & F . b < F . d & b,d are_adjacent & not a,d are_adjacent ) );