let NT be NTopSpace; :: thesis: for A, B being Subset of NT st A c= B holds
Int A c= Int B
let A, B be Subset of NT; :: thesis: ( A c= B implies Int A c= Int B )
assume A1: A c= B ; :: thesis: Int A c= Int B
Int A c= A by Lm15;
then Int A c= B by A1;
hence Int A c= Int B by Lm16; :: thesis: verum