let N be complete meet-continuous Lawson 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 A1: A in lambda N ; :: thesis: uparrow A in sigma S
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 ;
reconsider UA = uparrow A as Subset of S by A2;
A3: uparrow A = uparrow Y by A2, WAYBEL_0:13;
A4: S is meet-continuous by A2, YELLOW12:14;
A is open by A1, Th12;
then Y is property(S) by A2, WAYBEL19:36, YELLOW12:19;
then uparrow Y is property(S) by A4;
then UA is open by A3, WAYBEL11:15;
then uparrow A in the topology of S by PRE_TOPC:def 5;
hence uparrow A in sigma S by WAYBEL14:23; :: thesis: verum