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;
per cases ( L is being_line or ex x being Element of REAL 2 st L = {x} ) by Th6;
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;
suppose ex x being Element of REAL 2 st L = {x} ; :: thesis: contradiction
then consider x being Element of REAL 2 such that
A5: L = {x} ;
( Ox in {x} & Oy in {x} ) by A5, A1;
then ( Ox = x & Oy = x ) by TARSKI:def 1;
hence contradiction by Th14; :: thesis: verum
end;
end;