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