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: the topology of P = lambda [:M,N:] by WAYBEL19:def 4
.= the topology of [:Q,R:] by A1, Th19 ;
A3: RelStr(# the carrier of Q, the InternalRel of Q #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4;
A4: RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;
RelStr(# the carrier of P, the InternalRel of P #) = RelStr(# the carrier of [:M,N:], the InternalRel of [:M,N:] #) by YELLOW_9:def 4;
then the carrier of P = [: the carrier of Q, the carrier of N:] by A3, YELLOW_3:def 2
.= the carrier of [:Q,R:] by A4, BORSUK_1:def 2 ;
hence TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] by A2; :: thesis: verum