theorem Th75: :: EUCLIDLP:75

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds
L1 <> L2