let L1, L2 be Element of line_of_REAL 2; :: thesis: L1,L2 are_coplane
reconsider OO = |[0,0]|, Ox = |[1,0]|, Oy = |[0,1]| as Element of REAL 2 by EUCLID:22;
REAL 2 = plane (OO,Ox,Oy) by Th12;
hence L1,L2 are_coplane by EUCLIDLP:def 12; :: thesis: verum