for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n)
for L1, L2 being Element of line_of_REAL n st An <> Bn & An <> Cn & |((An - Bn),(An - Cn))| = 0 & L1 = Line (An,Bn) & L2 = Line (An,Cn) holds
L1 _|_ L2