let n be Nat; :: thesis: for L1, L2 being Element of line_of_REAL n holds
( L1 meets L2 iff ex x being Element of REAL n st
( x in L1 & x in L2 ) )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 meets L2 iff ex x being Element of REAL n st
( x in L1 & x in L2 ) )
thus ( L1 meets L2 implies ex x being Element of REAL n st
( x in L1 & x in L2 ) ) :: thesis: ( ex x being Element of REAL n st
( x in L1 & x in L2 ) implies L1 meets L2 )
proof
assume L1 meets L2 ; :: thesis: ex x being Element of REAL n st
( x in L1 & x in L2 )
then consider x being object such that
A1: x in L1 and
A2: x in L2 by XBOOLE_0:3;
reconsider x = x as Element of REAL n by A1;
take x ; :: thesis: ( x in L1 & x in L2 )
thus ( x in L1 & x in L2 ) by A1, A2; :: thesis: verum
end;
thus ( ex x being Element of REAL n st
( x in L1 & x in L2 ) implies L1 meets L2 ) by XBOOLE_0:3; :: thesis: verum