let N be complete Lawson meet-continuous TopLattice; :: thesis: for S being Scott TopAugmentation of N
for A being Subset of N st A in lambda N holds
uparrow A in sigma S
let S be Scott TopAugmentation of N; :: thesis: for A being Subset of N st A in lambda N holds
uparrow A in sigma S
let A be Subset of N; :: thesis: ( A in lambda N implies uparrow A in sigma S )
assume A in lambda N ; :: thesis: uparrow A in sigma S
then A1: A is open by Th12;
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
then reconsider Y = A as Subset of S ;
A3: S is meet-continuous by A2, YELLOW12:14;
reconsider UA = uparrow A as Subset of S by A2;
A4: uparrow A = uparrow Y by A2, WAYBEL_0:13;
Y is property(S) by A1, A2, WAYBEL19:36, YELLOW12:19;
then UA is open by A3, A4, WAYBEL11:15;
then uparrow A in the topology of S ;
hence uparrow A in sigma S by WAYBEL14:23; :: thesis: verum