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

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