theorem :: EUCLID12:19

for L1 being Element of line_of_REAL 2 ex L being Element of line_of_REAL 2 st
( L is being_point & L misses L1 )