theorem Th31: :: EUCLID12:39

for L1, L2 being Element of line_of_REAL 2 holds L1,L2 are_coplane