:: deftheorem defines with_property_L3 LEXBFS:def 18 :
for G being _Graph
for F being PartFunc of (the_Vertices_of G),NAT holds
( F is with_property_L3 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 . c < F . 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
F . e < F . d ) ) );