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 5 ;
hence TopStruct(# the carrier of P,the topology of P #) = [:Q,R:] by A2; :: thesis: verum