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 )
consider S being Scott TopAugmentation of T, R being correct lower TopAugmentation of T;
A1: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of T,the InternalRel of T #) ) by YELLOW_9:def 4;
T is TopAugmentation of T by YELLOW_9:44;
then A2: T is Refinement of S,R by Th29;
then A3: T is Refinement of R,S 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 S by A1;
reconsider z = x as Element of R by A1;
( downarrow y = downarrow x & downarrow y is closed & uparrow z = uparrow x & uparrow z is closed ) by A1, Th4, WAYBEL11:11, WAYBEL_0:13;
hence ( uparrow x is closed & downarrow x is closed ) by A1, A2, A3, Th21; :: thesis: {x} is closed
then (uparrow x) /\ (downarrow x) is closed by TOPS_1:35;
hence {x} is closed by Th28; :: thesis: verum