let N be complete Lawson meet-continuous TopLattice; :: thesis: ( N is continuous iff ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) )
set S = the Scott TopAugmentation of N;
A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) by YELLOW_9:def 4;
hereby :: thesis: ( N is with_open_semilattices & InclPoset (sigma N) is continuous implies N is continuous )
assume A2: N is continuous ; :: thesis: ( N is with_open_semilattices & InclPoset (sigma N) is continuous )
for x being Point of the Scott TopAugmentation of N ex J being Basis of x st
for W being Subset of the Scott TopAugmentation of N st W in J holds
W is Filter of the Scott TopAugmentation of N
proof
let x be Point of the Scott TopAugmentation of N; :: thesis: ex J being Basis of x st
for W being Subset of the Scott TopAugmentation of N st W in J holds
W is Filter of the Scott TopAugmentation of N
consider J being Basis of x such that
A3: for W being Subset of the Scott TopAugmentation of N st W in J holds
( W is open & W is filtered ) by A2, WAYBEL14:35;
take J ; :: thesis: for W being Subset of the Scott TopAugmentation of N st W in J holds
W is Filter of the Scott TopAugmentation of N
let W be Subset of the Scott TopAugmentation of N; :: thesis: ( W in J implies W is Filter of the Scott TopAugmentation of N )
assume A4: W in J ; :: thesis: W is Filter of the Scott TopAugmentation of N
then W is open by A3;
hence W is Filter of the Scott TopAugmentation of N by A3, A4, WAYBEL11:def 4, YELLOW_8:12; :: thesis: verum
end;
hence N is with_open_semilattices by Th32; :: thesis: InclPoset (sigma N) is continuous
InclPoset (sigma the Scott TopAugmentation of N) is continuous by A2, WAYBEL14:36;
hence InclPoset (sigma N) is continuous by A1, YELLOW_9:52; :: thesis: verum
end;
assume that
A5: N is with_open_semilattices and
A6: InclPoset (sigma N) is continuous ; :: thesis: N is continuous
A7: for x being Element of the Scott TopAugmentation of N ex J being Basis of x st
for Y being Subset of the Scott TopAugmentation of N st Y in J holds
( Y is open & Y is filtered )
proof
let x be Element of the Scott TopAugmentation of N; :: thesis: ex J being Basis of x st
for Y being Subset of the Scott TopAugmentation of N st Y in J holds
( Y is open & Y is filtered )
reconsider y = x as Element of N by A1;
consider J being Basis of y such that
A8: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A5;
reconsider J9 = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16;
take J9 ; :: thesis: for Y being Subset of the Scott TopAugmentation of N st Y in J9 holds
( Y is open & Y is filtered )
let Y be Subset of the Scott TopAugmentation of N; :: thesis: ( Y in J9 implies ( Y is open & Y is filtered ) )
assume A9: Y in J9 ; :: thesis: ( Y is open & Y is filtered )
then consider A being Subset of N such that
A10: Y = uparrow A and
A11: A in J ;
subrelstr A is meet-inheriting by A8, A11;
then A is filtered by YELLOW12:26;
hence ( Y is open & Y is filtered ) by A1, A9, A10, WAYBEL_0:4, YELLOW_8:12; :: thesis: verum
end;
sigma the Scott TopAugmentation of N = sigma N by A1, YELLOW_9:52;
then for x being Element of the Scott TopAugmentation of N holds x = "\/" ( { (inf X) where X is Subset of the Scott TopAugmentation of N : ( x in X & X in sigma the Scott TopAugmentation of N ) } , the Scott TopAugmentation of N) by A7, A6, WAYBEL14:37;
then the Scott TopAugmentation of N is continuous by WAYBEL14:38;
hence N is continuous by A1, YELLOW12:15; :: thesis: verum