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