let N be complete Lawson meet-continuous TopLattice; :: thesis: ( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) )
set S = the Scott TopAugmentation of N;
A1: RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;
hereby :: thesis: ( N is with_open_semilattices & InclPoset (sigma N) is algebraic implies N is algebraic )
assume A2: N is algebraic ; :: thesis: ( N is with_open_semilattices & InclPoset (sigma N) is algebraic )
then reconsider M = N as algebraic LATTICE ;
M is continuous ;
hence N is with_open_semilattices ; :: thesis: InclPoset (sigma N) is algebraic
the Scott TopAugmentation of N is algebraic by A1, A2, WAYBEL_8:17;
then ex K being Basis of the Scott TopAugmentation of N st K = { (uparrow x) where x is Element of the Scott TopAugmentation of N : x in the carrier of (CompactSublatt the Scott TopAugmentation of N) } by WAYBEL14:42;
then InclPoset (sigma the Scott TopAugmentation of N) is algebraic by WAYBEL14:43;
hence InclPoset (sigma N) is algebraic by A1, YELLOW_9:52; :: thesis: verum
end;
assume that
A3: N is with_open_semilattices and
A4: InclPoset (sigma N) is algebraic ; :: thesis: N is algebraic
reconsider T = InclPoset (sigma N) as algebraic LATTICE by A4;
T is continuous ;
then N is continuous by A3, Th35;
then for x being Element of the Scott TopAugmentation of N ex K being Basis of x st
for Y being Subset of the Scott TopAugmentation of N st Y in K holds
( Y is open & Y is filtered ) by WAYBEL14:35;
then A5: for V being Element of (InclPoset (sigma the Scott TopAugmentation of N)) ex VV being Subset of (InclPoset (sigma the Scott TopAugmentation of N)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma the Scott TopAugmentation of N)) st W in VV holds
W is co-prime ) ) by WAYBEL14:39;
InclPoset (sigma the Scott TopAugmentation of N) is algebraic by A1, A4, YELLOW_9:52;
then ex K being Basis of the Scott TopAugmentation of N st K = { (uparrow x) where x is Element of the Scott TopAugmentation of N : x in the carrier of (CompactSublatt the Scott TopAugmentation of N) } by A5, WAYBEL14:44;
then the Scott TopAugmentation of N is algebraic by WAYBEL14:45;
hence N is algebraic by A1, WAYBEL_8:17; :: thesis: verum