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 )
set S = the Scott TopAugmentation of T;
A1: T is TopAugmentation of the Scott TopAugmentation of T by YELLOW_9:45;
A2: 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 v = x as Element of the Scott TopAugmentation of T ;
wayabove v is open by WAYBEL11:36;
hence wayabove x is open by A2, A1, Th37, YELLOW12:13; :: thesis: (wayabove x) ` is closed
hence (wayabove x) ` is closed ; :: thesis: verum