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