let N be complete Lawson TopLattice; for T being complete LATTICE
for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
let T be complete LATTICE; for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
let A be correct Lawson TopAugmentation of T; ( RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) implies TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) )
assume A1:
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #)
; TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
A2:
omega T = omega N
by A1, WAYBEL19:3;
set S = the correct Scott TopAugmentation of T;
set l = the correct lower TopAugmentation of T;
A3:
RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
A4:
RelStr(# the carrier of the correct Scott TopAugmentation of T, the InternalRel of the correct Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T c= bool the carrier of N
then reconsider X = the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T as Subset-Family of N ;
reconsider X = X as Subset-Family of N ;
A5:
the topology of the correct lower TopAugmentation of T = omega T
by WAYBEL19:def 2;
(sigma N) \/ (omega N) is prebasis of N
by WAYBEL19:def 3;
then A6:
(sigma T) \/ (omega N) is prebasis of N
by A1, YELLOW_9:52;
A7:
the topology of the correct Scott TopAugmentation of T = sigma T
by YELLOW_9:51;
the carrier of N = the carrier of the correct Scott TopAugmentation of T \/ the carrier of the correct lower TopAugmentation of T
by A1, A4, A3;
then
N is Refinement of the correct Scott TopAugmentation of T, the correct lower TopAugmentation of T
by A2, A6, A5, A7, YELLOW_9:def 6;
then A8: the topology of N =
UniCl (FinMeetCl X)
by YELLOW_9:56
.=
lambda T
by A1, A5, A7, WAYBEL19:33
.=
the topology of A
by WAYBEL19:def 4
;
RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #)
by A1, YELLOW_9:def 4;
hence
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
by A8; verum