for X being OrtAfPl
for a, b being Element of X ex c being Element of X st
( LIN a,b,c & a <> c & b <> c )