for S, T being non empty lower-bounded Poset
for S9 being correct lower TopAugmentation of S
for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:]