let n be Nat; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 misses L2 holds
ex x being Element of REAL n st
( x in L1 & not x in L2 )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 misses L2 implies ex x being Element of REAL n st
( x in L1 & not x in L2 ) )
assume A1: L1 misses L2 ; :: thesis: ex x being Element of REAL n st
( x in L1 & not x in L2 )
consider x being Element of REAL n such that
A2: x in L1 by Th52;
take x ; :: thesis: ( x in L1 & not x in L2 )
thus ( x in L1 & not x in L2 ) by A1, A2, Th49; :: thesis: verum