let L be Element of line_of_REAL 2; :: thesis: not for x being Element of REAL 2 holds x in L

assume A1: for x being Element of REAL 2 holds x in L ; :: thesis: contradiction

reconsider OO = |[0,0]|, Ox = |[1,0]|, Oy = |[0,1]| as Element of REAL 2 by EUCLID:22;

A2: ( OO in L & Ox in L & Oy in L ) by A1;

assume A1: for x being Element of REAL 2 holds x in L ; :: thesis: contradiction

reconsider OO = |[0,0]|, Ox = |[1,0]|, Oy = |[0,1]| as Element of REAL 2 by EUCLID:22;

A2: ( OO in L & Ox in L & Oy in L ) by A1;

per cases
( L is being_line or ex x being Element of REAL 2 st L = {x} )
by Th6;

end;

suppose
L is being_line
; :: thesis: contradiction

then
L = Line (Ox,Oy)
by A2, Th14, EUCLIDLP:30;

then OO in { (((1 - lambda) * Ox) + (lambda * Oy)) where lambda is Real : verum } by A1;

then consider lambda being Real such that

A3: OO = ((1 - lambda) * Ox) + (lambda * Oy) ;

A4: |[0,0]| = ((1 - lambda) * |[1,0]|) + (lambda * |[0,1]|) by A3

.= |[((1 - lambda) * 1),((1 - lambda) * 0)]| + (lambda * |[0,1]|) by EUCLID:58

.= |[(1 - lambda),0]| + |[(lambda * 0),(lambda * 1)]| by EUCLID:58

.= |[((1 - lambda) + 0),(0 + lambda)]| by EUCLID:56

.= |[(1 - lambda),lambda]| ;

( |[0,0]| `1 = 0 & |[0,0]| `2 = 0 & |[(1 - lambda),lambda]| `1 = 1 - lambda & |[(1 - lambda),lambda]| `2 = lambda ) by EUCLID:52;

hence contradiction by A4; :: thesis: verum

end;then OO in { (((1 - lambda) * Ox) + (lambda * Oy)) where lambda is Real : verum } by A1;

then consider lambda being Real such that

A3: OO = ((1 - lambda) * Ox) + (lambda * Oy) ;

A4: |[0,0]| = ((1 - lambda) * |[1,0]|) + (lambda * |[0,1]|) by A3

.= |[((1 - lambda) * 1),((1 - lambda) * 0)]| + (lambda * |[0,1]|) by EUCLID:58

.= |[(1 - lambda),0]| + |[(lambda * 0),(lambda * 1)]| by EUCLID:58

.= |[((1 - lambda) + 0),(0 + lambda)]| by EUCLID:56

.= |[(1 - lambda),lambda]| ;

( |[0,0]| `1 = 0 & |[0,0]| `2 = 0 & |[(1 - lambda),lambda]| `1 = 1 - lambda & |[(1 - lambda),lambda]| `2 = lambda ) by EUCLID:52;

hence contradiction by A4; :: thesis: verum