let N be complete Lawson TopLattice; :: thesis: for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J & J is closed holds
A is closed
let S be Scott TopAugmentation of N; :: thesis: for A being Subset of N
for J being Subset of S st A = J & J is closed holds
A is closed
let A be Subset of N; :: thesis: for J being Subset of S st A = J & J is closed holds
A is closed
let J be Subset of S; :: thesis: ( A = J & J is closed implies A is closed )
assume A1: A = J ; :: thesis: ( not J is closed or A is closed )
assume J is closed ; :: thesis: A is closed
then A2: ([#] S) \ J is open ;
A3: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
then N is correct Lawson TopAugmentation of S by YELLOW_9:def 4;
hence ([#] N) \ A is open by A1, A3, A2, WAYBEL19:37; :: according to PRE_TOPC:def 3 :: thesis: verum