theorem :: EUCLID12:21

for L1, L2 being Element of line_of_REAL 2 holds
( L1 // L2 or L1 is being_point or L2 is being_point or ( L1 is being_line & L2 is being_line & L1 /\ L2 is being_point ) ) by Th16;