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 ;
now :: thesis: not L meets L1
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;
hence ex L being Element of line_of_REAL 2 st
( L is being_point & L misses L1 ) by A2; :: thesis: verum