let NT be NTopSpace; :: thesis: for A, B being Subset of NT st A misses B holds
Int A misses Int B
let A, B be Subset of NT; :: thesis: ( A misses B implies Int A misses Int B )
assume A1: A misses B ; :: thesis: Int A misses Int B
( Int A c= A & Int B c= B ) by Lm15;
then (Int A) /\ (Int B) c= {} by A1, XBOOLE_1:27;
hence Int A misses Int B ; :: thesis: verum