for AS being AffinSpace
for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )