let V be RealLinearSpace; :: thesis: for A, B being Subset of V st A c< B holds

conv A misses Int B

let A, B be Subset of V; :: thesis: ( A c< B implies conv A misses Int B )

assume A1: A c< B ; :: thesis: conv A misses Int B

assume conv A meets Int B ; :: thesis: contradiction

then ex x being object st

( x in conv A & x in Int B ) by XBOOLE_0:3;

hence contradiction by A1, Def1; :: thesis: verum

conv A misses Int B

let A, B be Subset of V; :: thesis: ( A c< B implies conv A misses Int B )

assume A1: A c< B ; :: thesis: conv A misses Int B

assume conv A meets Int B ; :: thesis: contradiction

then ex x being object st

( x in conv A & x in Int B ) by XBOOLE_0:3;

hence contradiction by A1, Def1; :: thesis: verum