let M, N be complete LATTICE; :: thesis: 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:]
let P be correct Lawson TopAugmentation of [:M,N:]; :: thesis: 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:]
let Q be correct Lawson TopAugmentation of M; :: thesis: 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:]
let R be correct Lawson TopAugmentation of N; :: thesis: ( InclPoset (sigma N) is continuous implies TopStruct(# the carrier of P,the topology of P #) = [:Q,R:] )
assume A1: InclPoset (sigma N) is continuous ; :: thesis: TopStruct(# the carrier of P,the topology of P #) = [:Q,R:]
A2: ( RelStr(# the carrier of P,the InternalRel of P #) = RelStr(# the carrier of [:M,N:],the InternalRel of [:M,N:] #) & RelStr(# the carrier of Q,the InternalRel of Q #) = RelStr(# the carrier of M,the InternalRel of M #) & RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of N,the InternalRel of N #) ) by YELLOW_9:def 4;
then A3: the carrier of P = [:the carrier of Q,the carrier of N:] by YELLOW_3:def 2
.= the carrier of [:Q,R:] by A2, BORSUK_1:def 5 ;
the topology of P = lambda [:M,N:] by WAYBEL19:def 4
.= the topology of [:Q,R:] by A1, Th19 ;
hence TopStruct(# the carrier of P,the topology of P #) = [:Q,R:] by A3; :: thesis: verum