let x be Element of REAL 2; :: thesis: for L1 being Element of line_of_REAL 2 st L1 is being_line holds

ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 )

let L1 be Element of line_of_REAL 2; :: thesis: ( L1 is being_line implies ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 ) )

assume A1: L1 is being_line ; :: thesis: ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 )

ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 )

let L1 be Element of line_of_REAL 2; :: thesis: ( L1 is being_line implies ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 ) )

assume A1: L1 is being_line ; :: thesis: ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 )

per cases
( x in L1 or not x in L1 )
;

end;

suppose
x in L1
; :: thesis: ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 )

( x in L2 & L1 _|_ L2 )

consider x1 being Element of REAL 2 such that

A2: not x1 in L1 by Th15;

consider L2 being Element of line_of_REAL 2 such that

x1 in L2 and

A3: L1 _|_ L2 and

L1 meets L2 by A1, A2, EUCLIDLP:62;

consider L3 being Element of line_of_REAL 2 such that

A4: x in L3 and

A5: L3 _|_ L1 and

L3 // L2 by A3, EUCLIDLP:80;

thus ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 ) by A4, A5; :: thesis: verum

end;A2: not x1 in L1 by Th15;

consider L2 being Element of line_of_REAL 2 such that

x1 in L2 and

A3: L1 _|_ L2 and

L1 meets L2 by A1, A2, EUCLIDLP:62;

consider L3 being Element of line_of_REAL 2 such that

A4: x in L3 and

A5: L3 _|_ L1 and

L3 // L2 by A3, EUCLIDLP:80;

thus ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 ) by A4, A5; :: thesis: verum

suppose
not x in L1
; :: thesis: ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 )

( x in L2 & L1 _|_ L2 )

then consider L2 being Element of line_of_REAL 2 such that

A6: x in L2 and

A7: L1 _|_ L2 and

L1 meets L2 by A1, EUCLIDLP:62;

thus ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 ) by A6, A7; :: thesis: verum

end;A6: x in L2 and

A7: L1 _|_ L2 and

L1 meets L2 by A1, EUCLIDLP:62;

thus ex L2 being Element of line_of_REAL 2 st

( x in L2 & L1 _|_ L2 ) by A6, A7; :: thesis: verum