let T be complete continuous Lawson TopLattice; :: thesis: for x being Element of T holds
( wayabove x is open & (wayabove x) ` is closed )
let x be Element of T; :: thesis: ( wayabove x is open & (wayabove x) ` is closed )
consider S being Scott TopAugmentation of T;
A1: T is TopAugmentation of S by YELLOW_9:45;
A2: 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 v = x as Element of S ;
wayabove v is open by WAYBEL11:36;
hence wayabove x is open by A2, YELLOW12:13, A1, Th37; :: thesis: (wayabove x) ` is closed
hence (wayabove x) ` is closed by TOPS_1:30; :: thesis: verum