theorem Th4: :: CONMETR:4
for X being OrtAfPl
for a, b, c being Element of X
for A being Subset of X st A is being_line & a in A & b in A & c in A holds
LIN a,b,c