let R be complete LATTICE; for LL being correct lower TopAugmentation of R
for S being Scott TopAugmentation of R
for T being correct TopAugmentation of R holds
( T is Lawson iff T is Refinement of S,LL )
let LL be correct lower TopAugmentation of R; for S being Scott TopAugmentation of R
for T being correct TopAugmentation of R holds
( T is Lawson iff T is Refinement of S,LL )
let S be Scott TopAugmentation of R; for T being correct TopAugmentation of R holds
( T is Lawson iff T is Refinement of S,LL )
let T be correct TopAugmentation of R; ( T is Lawson iff T is Refinement of S,LL )
A1:
the topology of S = sigma R
by YELLOW_9:51;
A2:
the carrier of R \/ the carrier of R = the carrier of R
;
A3:
the topology of LL = omega R
by Def2;
A4:
RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of R, the InternalRel of R #)
by YELLOW_9:def 4;
A5:
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #)
by YELLOW_9:def 4;
A6:
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #)
by YELLOW_9:def 4;
then A7:
sigma T = sigma R
by YELLOW_9:52;
omega T = omega R
by A6, Th3;
hence
( T is Lawson iff T is Refinement of S,LL )
by A7, A3, A1, A2, A4, A5, A6, YELLOW_9:def 6; verum