:: deftheorem defines satisfying_TDES_3 AFF_2:def 10 :
for AP being AffinPlane holds
( AP is satisfying_TDES_3 iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & a,b // K holds
c9 in K );