let X be TopSpace; :: thesis: for B, A being Subset of X st B is boundary & A c= B holds
A is boundary
let B, A be Subset of X; :: thesis: ( B is boundary & A c= B implies A is boundary )
assume B is boundary ; :: thesis: ( not A c= B or A is boundary )
then A1: Int B = {} ;
assume A c= B ; :: thesis: A is boundary
then Int A = {} by A1, TOPS_1:19, XBOOLE_1:3;
hence A is boundary by TOPS_1:48; :: thesis: verum