let S, T be non empty lower-bounded lower TopPoset; :: thesis: omega [:S,T:] = the topology of [:S,T:]
( S is TopAugmentation of S & T is TopAugmentation of T ) by YELLOW_9:44;
hence omega [:S,T:] = the topology of [:S,T:] by Th15; :: thesis: verum