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