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 )
A2: RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of S,the InternalRel of S #) by YELLOW_9:def 4;
assume J is closed ; :: thesis: A is closed
then A3: ([#] S) \ J is open by PRE_TOPC:def 6;
N is correct Lawson TopAugmentation of S by A2, YELLOW_9:def 4;
hence ([#] N) \ A is open by A1, A2, A3, WAYBEL19:37; :: according to PRE_TOPC:def 6 :: thesis: verum