let N be complete Lawson meet-continuous TopLattice; :: thesis: for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J & A is open holds
uparrow J is open
let S be Scott TopAugmentation of N; :: thesis: for A being Subset of N
for J being Subset of S st A = J & A is open holds
uparrow J is open
let A be Subset of N; :: thesis: for J being Subset of S st A = J & A is open holds
uparrow J is open
let J be Subset of S; :: thesis: ( A = J & A is open implies uparrow J is open )
assume A1: A = J ; :: thesis: ( not A is open or uparrow J is open )
assume A is open ; :: thesis: uparrow J is open
then A in lambda N by Th12;
then A2: uparrow A in sigma S by Th14;
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
then uparrow J in sigma S by A2, A1, WAYBEL_0:13;
hence uparrow J is open by WAYBEL14:24; :: thesis: verum