theorem Th33: :: EUCLID12:43

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 holds
ex x being Element of REAL 2 st L1 /\ L2 = {x}