let X1, X2 be TopSpace; :: thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
let D1 be Subset of X1; :: thesis: for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
let D2 be Subset of X2; :: thesis: ( D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary implies D2 is boundary )
assume A1: D2 c= D1 ; :: thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is boundary or D2 is boundary )
then reconsider C1 = D2 as Subset of X1 by XBOOLE_1:1;
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; :: thesis: ( not D1 is boundary or D2 is boundary )
assume D1 is boundary ; :: thesis: D2 is boundary
then C1 is boundary by A1, Th11;
then A3: Int C1 = {} ;
Int C1 = Int D2 by A2, Th77;
hence D2 is boundary by A3; :: thesis: verum