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;
let x be Element of T; :: thesis: ( uparrow x is closed & downarrow x is closed & {x} is closed )
A1: 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 #) by YELLOW_9:def 4;
then reconsider y = x as Element of the Scott TopAugmentation of T ;
A2: downarrow y is closed by WAYBEL11:11;
T is TopAugmentation of T by YELLOW_9:44;
then A3: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29;
A4: 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;
then reconsider z = x as Element of the correct lower TopAugmentation of T ;
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