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