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