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