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

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