let n be Nat; :: thesis: for x0 being Element of REAL n
for L being Element of line_of_REAL n st L is being_line holds
ex x1 being Element of REAL n st
( x1 <> x0 & x1 in L )
let x0 be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st L is being_line holds
ex x1 being Element of REAL n st
( x1 <> x0 & x1 in L )
let L be Element of line_of_REAL n; :: thesis: ( L is being_line implies ex x1 being Element of REAL n st
( x1 <> x0 & x1 in L ) )
assume L is being_line ; :: thesis: ex x1 being Element of REAL n st
( x1 <> x0 & x1 in L )
then consider y1, y2 being Element of REAL n such that
A1: y1 in L and
A2: ( y2 in L & y1 <> y2 ) by EUCLID_4:13;
now :: thesis: ( ( y1 = x0 & ex y2 being Element of REAL n st
( y2 <> x0 & y2 in L ) ) or ( y1 <> x0 & ex y1 being Element of REAL n st
( y1 <> x0 & y1 in L ) ) )
per cases ( y1 = x0 or y1 <> x0 ) ;
case A3: y1 = x0 ; :: thesis: ex y2 being Element of REAL n st
( y2 <> x0 & y2 in L )
take y2 = y2; :: thesis: ( y2 <> x0 & y2 in L )
thus ( y2 <> x0 & y2 in L ) by A2, A3; :: thesis: verum
end;
case A4: y1 <> x0 ; :: thesis: ex y1 being Element of REAL n st
( y1 <> x0 & y1 in L )
take y1 = y1; :: thesis: ( y1 <> x0 & y1 in L )
thus ( y1 <> x0 & y1 in L ) by A1, A4; :: thesis: verum
end;
end;
end;
hence ex x1 being Element of REAL n st
( x1 <> x0 & x1 in L ) ; :: thesis: verum