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 )
per cases ( x in L1 or not x in L1 ) ;
suppose x in L1 ; :: thesis: ex L2 being Element of line_of_REAL 2 st
( 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;
suppose not x in L1 ; :: thesis: ex L2 being Element of line_of_REAL 2 st
( 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;
end;