let n be Nat; :: thesis: for A being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds
A = Line (p1,p2)
let A be Subset of (TOP-REAL n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds
A = Line (p1,p2)
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( A is being_line & p1 in A & p2 in A & p1 <> p2 implies A = Line (p1,p2) )
assume that
A1: A is being_line and
A2: ( p1 in A & p2 in A & p1 <> p2 ) ; :: thesis: A = Line (p1,p2)
ex q1, q2 being Point of (TOP-REAL n) st
( q1 <> q2 & A = Line (q1,q2) ) by A1, Def8;
then ( Line (p1,p2) c= A & A c= Line (p1,p2) ) by A2, Th48, Th49;
hence A = Line (p1,p2) by XBOOLE_0:def 10; :: thesis: verum