theorem Th20: :: WAYBEL30:20

for M, N being complete LATTICE
for P being correct Lawson TopAugmentation of [:M,N:]
for Q being correct Lawson TopAugmentation of M
for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]