let M, N be complete LATTICE; :: thesis: for LM being correct Lawson TopAugmentation of M

for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds

the topology of [:LM,LN:] = lambda [:M,N:]

let LM be correct Lawson TopAugmentation of M; :: thesis: for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds

the topology of [:LM,LN:] = lambda [:M,N:]

let LN be correct Lawson TopAugmentation of N; :: thesis: ( InclPoset (sigma N) is continuous implies the topology of [:LM,LN:] = lambda [:M,N:] )

assume A1: InclPoset (sigma N) is continuous ; :: thesis: the topology of [:LM,LN:] = lambda [:M,N:]

set SMN = the non empty correct Scott TopAugmentation of [:M,N:];

set lMN = the non empty correct lower TopAugmentation of [:M,N:];

set LMN = the non empty correct Lawson TopAugmentation of [:M,N:];

A2: [:LM,LN:] = TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #)

then reconsider R = [:LM,LN:] as Refinement of the non empty correct Scott TopAugmentation of [:M,N:], the non empty correct lower TopAugmentation of [:M,N:] by A2, YELLOW12:47;

the topology of [:LM,LN:] = the topology of R ;

hence the topology of [:LM,LN:] = lambda [:M,N:] by WAYBEL19:34; :: thesis: verum

for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds

the topology of [:LM,LN:] = lambda [:M,N:]

let LM be correct Lawson TopAugmentation of M; :: thesis: for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds

the topology of [:LM,LN:] = lambda [:M,N:]

let LN be correct Lawson TopAugmentation of N; :: thesis: ( InclPoset (sigma N) is continuous implies the topology of [:LM,LN:] = lambda [:M,N:] )

assume A1: InclPoset (sigma N) is continuous ; :: thesis: the topology of [:LM,LN:] = lambda [:M,N:]

set SMN = the non empty correct Scott TopAugmentation of [:M,N:];

set lMN = the non empty correct lower TopAugmentation of [:M,N:];

set LMN = the non empty correct Lawson TopAugmentation of [:M,N:];

A2: [:LM,LN:] = TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #)

proof

the non empty correct Lawson TopAugmentation of [:M,N:] is Refinement of the non empty correct Scott TopAugmentation of [:M,N:], the non empty correct lower TopAugmentation of [:M,N:]
by WAYBEL19:29;
set lN = the non empty correct lower TopAugmentation of N;

set lM = the non empty correct lower TopAugmentation of M;

set SN = the non empty correct Scott TopAugmentation of N;

set SM = the non empty correct Scott TopAugmentation of M;

A3: LN is Refinement of the non empty correct Scott TopAugmentation of N, the non empty correct lower TopAugmentation of N by WAYBEL19:29;

A4: RelStr(# the carrier of the non empty correct lower TopAugmentation of N, the InternalRel of the non empty correct lower TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;

(omega the non empty correct Lawson TopAugmentation of [:M,N:]) \/ (sigma the non empty correct Lawson TopAugmentation of [:M,N:]) is prebasis of the non empty correct Lawson TopAugmentation of [:M,N:] by WAYBEL19:def 3;

then A5: (omega the non empty correct Lawson TopAugmentation of [:M,N:]) \/ (sigma the non empty correct Lawson TopAugmentation of [:M,N:]) is prebasis of TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) by YELLOW12:33;

A6: RelStr(# the carrier of LM, the InternalRel of LM #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4;

A7: RelStr(# the carrier of LN, the InternalRel of LN #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;

A8: RelStr(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the InternalRel of the non empty correct Lawson TopAugmentation of [:M,N:] #) = RelStr(# the carrier of [:M,N:], the InternalRel of [:M,N:] #) by YELLOW_9:def 4;

A9: the carrier of [:LM,LN:] = [: the carrier of LM, the carrier of LN:] by BORSUK_1:def 2

.= the carrier of the non empty correct Lawson TopAugmentation of [:M,N:] by A6, A7, A8, YELLOW_3:def 2 ;

A10: the topology of [: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] = omega [:M,N:] by WAYBEL19:15

.= omega the non empty correct Lawson TopAugmentation of [:M,N:] by A8, WAYBEL19:3 ;

A11: RelStr(# the carrier of the non empty correct Scott TopAugmentation of N, the InternalRel of the non empty correct Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;

RelStr(# the carrier of the non empty correct Scott TopAugmentation of M, the InternalRel of the non empty correct Scott TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4

.= RelStr(# the carrier of (Sigma M), the InternalRel of (Sigma M) #) by YELLOW_9:def 4 ;

then A12: TopStruct(# the carrier of the non empty correct Scott TopAugmentation of M, the topology of the non empty correct Scott TopAugmentation of M #) = TopStruct(# the carrier of (Sigma M), the topology of (Sigma M) #) by WAYBEL29:13;

A13: RelStr(# the carrier of the non empty correct lower TopAugmentation of M, the InternalRel of the non empty correct lower TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4;

RelStr(# the carrier of the non empty correct Scott TopAugmentation of N, the InternalRel of the non empty correct Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4

.= RelStr(# the carrier of (Sigma N), the InternalRel of (Sigma N) #) by YELLOW_9:def 4 ;

then TopStruct(# the carrier of the non empty correct Scott TopAugmentation of N, the topology of the non empty correct Scott TopAugmentation of N #) = TopStruct(# the carrier of (Sigma N), the topology of (Sigma N) #) by WAYBEL29:13;

then A14: the topology of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:] = the topology of [:(Sigma M),(Sigma N):] by A12, WAYBEL29:7

.= sigma [:M,N:] by A1, WAYBEL29:30

.= sigma the non empty correct Lawson TopAugmentation of [:M,N:] by A8, YELLOW_9:52 ;

A15: RelStr(# the carrier of the non empty correct Scott TopAugmentation of M, the InternalRel of the non empty correct Scott TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4;

A16: LM is Refinement of the non empty correct Scott TopAugmentation of M, the non empty correct lower TopAugmentation of M by WAYBEL19:29;

then [:LM,LN:] is Refinement of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:],[: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A3, A15, A11, A13, A4, YELLOW12:50;

then the carrier of TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) = the carrier of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:] \/ the carrier of [: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A9, YELLOW_9:def 6;

then TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) is Refinement of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:],[: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A5, A14, A10, YELLOW_9:def 6;

hence [:LM,LN:] = TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) by A16, A3, A15, A11, A13, A4, A9, YELLOW12:49; :: thesis: verum

end;set lM = the non empty correct lower TopAugmentation of M;

set SN = the non empty correct Scott TopAugmentation of N;

set SM = the non empty correct Scott TopAugmentation of M;

A3: LN is Refinement of the non empty correct Scott TopAugmentation of N, the non empty correct lower TopAugmentation of N by WAYBEL19:29;

A4: RelStr(# the carrier of the non empty correct lower TopAugmentation of N, the InternalRel of the non empty correct lower TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;

(omega the non empty correct Lawson TopAugmentation of [:M,N:]) \/ (sigma the non empty correct Lawson TopAugmentation of [:M,N:]) is prebasis of the non empty correct Lawson TopAugmentation of [:M,N:] by WAYBEL19:def 3;

then A5: (omega the non empty correct Lawson TopAugmentation of [:M,N:]) \/ (sigma the non empty correct Lawson TopAugmentation of [:M,N:]) is prebasis of TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) by YELLOW12:33;

A6: RelStr(# the carrier of LM, the InternalRel of LM #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4;

A7: RelStr(# the carrier of LN, the InternalRel of LN #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;

A8: RelStr(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the InternalRel of the non empty correct Lawson TopAugmentation of [:M,N:] #) = RelStr(# the carrier of [:M,N:], the InternalRel of [:M,N:] #) by YELLOW_9:def 4;

A9: the carrier of [:LM,LN:] = [: the carrier of LM, the carrier of LN:] by BORSUK_1:def 2

.= the carrier of the non empty correct Lawson TopAugmentation of [:M,N:] by A6, A7, A8, YELLOW_3:def 2 ;

A10: the topology of [: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] = omega [:M,N:] by WAYBEL19:15

.= omega the non empty correct Lawson TopAugmentation of [:M,N:] by A8, WAYBEL19:3 ;

A11: RelStr(# the carrier of the non empty correct Scott TopAugmentation of N, the InternalRel of the non empty correct Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;

RelStr(# the carrier of the non empty correct Scott TopAugmentation of M, the InternalRel of the non empty correct Scott TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4

.= RelStr(# the carrier of (Sigma M), the InternalRel of (Sigma M) #) by YELLOW_9:def 4 ;

then A12: TopStruct(# the carrier of the non empty correct Scott TopAugmentation of M, the topology of the non empty correct Scott TopAugmentation of M #) = TopStruct(# the carrier of (Sigma M), the topology of (Sigma M) #) by WAYBEL29:13;

A13: RelStr(# the carrier of the non empty correct lower TopAugmentation of M, the InternalRel of the non empty correct lower TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4;

RelStr(# the carrier of the non empty correct Scott TopAugmentation of N, the InternalRel of the non empty correct Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4

.= RelStr(# the carrier of (Sigma N), the InternalRel of (Sigma N) #) by YELLOW_9:def 4 ;

then TopStruct(# the carrier of the non empty correct Scott TopAugmentation of N, the topology of the non empty correct Scott TopAugmentation of N #) = TopStruct(# the carrier of (Sigma N), the topology of (Sigma N) #) by WAYBEL29:13;

then A14: the topology of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:] = the topology of [:(Sigma M),(Sigma N):] by A12, WAYBEL29:7

.= sigma [:M,N:] by A1, WAYBEL29:30

.= sigma the non empty correct Lawson TopAugmentation of [:M,N:] by A8, YELLOW_9:52 ;

A15: RelStr(# the carrier of the non empty correct Scott TopAugmentation of M, the InternalRel of the non empty correct Scott TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def 4;

A16: LM is Refinement of the non empty correct Scott TopAugmentation of M, the non empty correct lower TopAugmentation of M by WAYBEL19:29;

then [:LM,LN:] is Refinement of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:],[: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A3, A15, A11, A13, A4, YELLOW12:50;

then the carrier of TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) = the carrier of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:] \/ the carrier of [: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A9, YELLOW_9:def 6;

then TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) is Refinement of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:],[: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A5, A14, A10, YELLOW_9:def 6;

hence [:LM,LN:] = TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) by A16, A3, A15, A11, A13, A4, A9, YELLOW12:49; :: thesis: verum

then reconsider R = [:LM,LN:] as Refinement of the non empty correct Scott TopAugmentation of [:M,N:], the non empty correct lower TopAugmentation of [:M,N:] by A2, YELLOW12:47;

the topology of [:LM,LN:] = the topology of R ;

hence the topology of [:LM,LN:] = lambda [:M,N:] by WAYBEL19:34; :: thesis: verum