let n be Nat; :: thesis: for x1 being Element of REAL n

for A being Subset of (REAL n) st A is being_line holds

ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A )

let x1 be Element of REAL n; :: thesis: for A being Subset of (REAL n) st A is being_line holds

ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A )

let A be Subset of (REAL n); :: thesis: ( A is being_line implies ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A ) )

assume A is being_line ; :: thesis: ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A )

then consider y1, y2 being Element of REAL n such that

A1: y1 in A and

A2: ( y2 in A & y1 <> y2 ) by Th13;

( x1 = y1 implies ( x1 <> y2 & y2 in A ) ) by A2;

hence ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A ) by A1; :: thesis: verum

for A being Subset of (REAL n) st A is being_line holds

ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A )

let x1 be Element of REAL n; :: thesis: for A being Subset of (REAL n) st A is being_line holds

ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A )

let A be Subset of (REAL n); :: thesis: ( A is being_line implies ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A ) )

assume A is being_line ; :: thesis: ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A )

then consider y1, y2 being Element of REAL n such that

A1: y1 in A and

A2: ( y2 in A & y1 <> y2 ) by Th13;

( x1 = y1 implies ( x1 <> y2 & y2 in A ) ) by A2;

hence ex x2 being Element of REAL n st

( x1 <> x2 & x2 in A ) by A1; :: thesis: verum