theorem Th35: :: EUCLID12:47

for x being Element of REAL 2
for L1 being Element of line_of_REAL 2 st L1 is being_line holds
ex L2 being Element of line_of_REAL 2 st
( x in L2 & L1 _|_ L2 )