let L1 be Element of line_of_REAL 2; :: thesis: ex L being Element of line_of_REAL 2 st

( L is being_point & L misses L1 )

consider x being Element of REAL 2 such that

A1: not x in L1 by Th15;

x in REAL 2 ;

then {x} c= REAL 2 by TARSKI:def 1;

then reconsider L = {x} as Subset of (REAL 2) ;

L = Line (x,x) by Th3;

then reconsider L = L as Element of line_of_REAL 2 by EUCLIDLP:47;

A2: L is being_point ;

( L is being_point & L misses L1 ) by A2; :: thesis: verum

( L is being_point & L misses L1 )

consider x being Element of REAL 2 such that

A1: not x in L1 by Th15;

x in REAL 2 ;

then {x} c= REAL 2 by TARSKI:def 1;

then reconsider L = {x} as Subset of (REAL 2) ;

L = Line (x,x) by Th3;

then reconsider L = L as Element of line_of_REAL 2 by EUCLIDLP:47;

A2: L is being_point ;

now :: thesis: not L meets L1

hence
ex L being Element of line_of_REAL 2 st assume
L meets L1
; :: thesis: contradiction

then consider y being object such that

A3: y in L and

A4: y in L1 by XBOOLE_0:3;

thus contradiction by A1, A3, A4, TARSKI:def 1; :: thesis: verum

end;then consider y being object such that

A3: y in L and

A4: y in L1 by XBOOLE_0:3;

thus contradiction by A1, A3, A4, TARSKI:def 1; :: thesis: verum

( L is being_point & L misses L1 ) by A2; :: thesis: verum