let T be complete Lawson TopLattice; :: thesis: for x being Element of T holds
( uparrow x is closed & downarrow x is closed & {x} is closed )
set S = the Scott TopAugmentation of T;
set R = the correct lower TopAugmentation of T;
A: ( RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) & 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;
T is TopAugmentation of T by YELLOW_9:44;
then C: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29;
then D: T is Refinement of the correct lower TopAugmentation of T, the Scott TopAugmentation of T by YELLOW_9:55;
let x be Element of T; :: thesis: ( uparrow x is closed & downarrow x is closed & {x} is closed )
reconsider y = x as Element of the Scott TopAugmentation of T by A;
reconsider z = x as Element of the correct lower TopAugmentation of T by A;
( downarrow y = downarrow x & downarrow y is closed & uparrow z = uparrow x & uparrow z is closed ) by A, WAYBEL_0:13, Th4, WAYBEL11:11;
hence ( uparrow x is closed & downarrow x is closed ) by A, C, D, Th21; :: thesis: {x} is closed
then (uparrow x) /\ (downarrow x) is closed ;
hence {x} is closed by Th28; :: thesis: verum