theorem Th50: :: AFPROJ:50

for AS being AffinSpace
for A, P, C being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds
b,c // b9,c9