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 LL = omega R by Def2;
A2: the topology of S = sigma R by YELLOW_9:51;
A3: ( (omega T) \/ (sigma T) is prebasis of T iff T is Lawson ) by Def3;
A4: the carrier of R \/ the carrier of R = the carrier of R ;
A5: ( RelStr(# the carrier of LL,the InternalRel of LL #) = RelStr(# the carrier of R,the InternalRel of R #) & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of R,the InternalRel of R #) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) ) by YELLOW_9:def 4;
then ( omega T = omega R & sigma T = sigma R ) by Th3, YELLOW_9:52;
hence ( T is Lawson iff T is Refinement of S,LL ) by A1, A2, A3, A4, A5, YELLOW_9:def 6; :: thesis: verum