let A, B be Point of (TOP-REAL 2); :: thesis: for L being Element of line_of_REAL 2 st L is being_line & A in L & B in L & A <> B holds
L = Line (A,B)
let L be Element of line_of_REAL 2; :: thesis: ( L is being_line & A in L & B in L & A <> B implies L = Line (A,B) )
assume A1: ( L is being_line & A in L & B in L & A <> B ) ; :: thesis: L = Line (A,B)
reconsider x1 = A, x2 = B as Element of REAL 2 by EUCLID:22;
L = Line (x1,x2) by A1, EUCLID_4:10, EUCLID_4:11;
hence L = Line (A,B) by Th4; :: thesis: verum