let T, S be TopSpace; :: thesis: for R being Refinement of T,S
for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds
W is open
let R be Refinement of T,S; :: thesis: for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds
W is open
let W be Subset of R; :: thesis: ( ( W in the topology of T or W in the topology of S ) implies W is open )
the topology of T \/ the topology of S is prebasis of R by YELLOW_9:def 6;
then A1: the topology of T \/ the topology of S c= the topology of R by TOPS_2:64;
assume ( W in the topology of T or W in the topology of S ) ; :: thesis: W is open
then W in the topology of T \/ the topology of S by XBOOLE_0:def 3;
hence W in the topology of R by A1; :: according to PRE_TOPC:def 2 :: thesis: verum