let R be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: verum