let T be TopSpace; :: thesis: for A, B being Subset of T st A misses B holds
Int A misses Int B
let A, B be Subset of T; :: 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 TOPS_1:16;
then (Int A) /\ (Int B) c= {} by A1, XBOOLE_1:27;
hence Int A misses Int B ; :: thesis: verum