:: WAYBEL30 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: WAYBEL30:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum }
proof end;

theorem Th2: :: WAYBEL30:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty reflexive transitive RelStr
for D being non empty directed Subset of (InclPoset (Ids R)) holds union D is Ideal of R
proof end;

Lm1: now
let R be non empty reflexive transitive RelStr ; :: thesis: for D being non empty directed Subset of (InclPoset (Ids R))
for UD being Element of (InclPoset (Ids R)) st UD = union D holds
D is_<=_than UD

let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds
D is_<=_than UD

let UD be Element of (InclPoset (Ids R)); :: thesis: ( UD = union D implies D is_<=_than UD )
assume A1: UD = union D ; :: thesis: D is_<=_than UD
thus D is_<=_than UD :: thesis: verum
proof
let d be Element of (InclPoset (Ids R)); :: according to LATTICE3:def 9 :: thesis: ( not d in D or d <= UD )
assume A2: d in D ; :: thesis: d <= UD
d c= UD
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in d or a in UD )
assume a in d ; :: thesis: a in UD
hence a in UD by A1, A2, TARSKI:def 4; :: thesis: verum
end;
hence d <= UD by YELLOW_1:3; :: thesis: verum
end;
end;

Lm2: now
let R be non empty reflexive transitive RelStr ; :: thesis: for D being non empty directed Subset of (InclPoset (Ids R))
for UD being Element of (InclPoset (Ids R)) st UD = union D holds
for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b

let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds
for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b

let UD be Element of (InclPoset (Ids R)); :: thesis: ( UD = union D implies for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b )

assume A1: UD = union D ; :: thesis: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b

thus for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b :: thesis: verum
proof
let b be Element of (InclPoset (Ids R)); :: thesis: ( b is_>=_than D implies UD <= b )
assume A2: for a being Element of (InclPoset (Ids R)) st a in D holds
b >= a ; :: according to LATTICE3:def 9 :: thesis: UD <= b
UD c= b
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UD or x in b )
assume x in UD ; :: thesis: x in b
then consider Z being set such that
A3: ( x in Z & Z in D ) by A1, TARSKI:def 4;
reconsider Z = Z as Element of (InclPoset (Ids R)) by A3;
b >= Z by A2, A3;
then Z c= b by YELLOW_1:3;
hence x in b by A3; :: thesis: verum
end;
hence UD <= b by YELLOW_1:3; :: thesis: verum
end;
end;

registration
let R be non empty reflexive transitive RelStr ;
cluster InclPoset (Ids R) -> up-complete ;
coherence
InclPoset (Ids R) is up-complete
proof end;
end;

theorem Th3: :: WAYBEL30:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty reflexive transitive RelStr
for D being non empty directed Subset of (InclPoset (Ids R)) holds sup D = union D
proof end;

theorem Th4: :: WAYBEL30:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Semilattice
for D being non empty directed Subset of (InclPoset (Ids R))
for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }
proof end;

registration
let R be Semilattice;
cluster InclPoset (Ids R) -> up-complete satisfying_MC ;
coherence
InclPoset (Ids R) is satisfying_MC
proof end;
end;

registration
let R be non empty trivial RelStr ;
cluster -> trivial TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is trivial
proof end;
end;

theorem :: WAYBEL30:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being complete Scott TopLattice
for T being complete LATTICE
for A being Scott TopAugmentation of T st RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) holds
TopRelStr(# the carrier of A,the InternalRel of A,the topology of A #) = TopRelStr(# the carrier of S,the InternalRel of S,the topology of S #)
proof end;

theorem :: WAYBEL30:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Lawson TopLattice
for T being complete LATTICE
for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of T,the InternalRel of T #) holds
TopRelStr(# the carrier of A,the InternalRel of A,the topology of A #) = TopRelStr(# the carrier of N,the InternalRel of N,the topology of N #)
proof end;

theorem :: WAYBEL30:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Lawson TopLattice
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
proof end;

registration
let A be complete LATTICE;
cluster lambda A -> non empty ;
coherence
not lambda A is empty
proof end;
end;

registration
let S be complete Scott TopLattice;
cluster InclPoset (sigma S) -> complete non trivial ;
coherence
( InclPoset (sigma S) is complete & not InclPoset (sigma S) is trivial )
proof end;
end;

registration
let N be complete Lawson TopLattice;
cluster InclPoset (sigma N) -> complete non trivial ;
coherence
( InclPoset (sigma N) is complete & not InclPoset (sigma N) is trivial )
proof end;
cluster InclPoset (lambda N) -> complete non trivial ;
coherence
( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial )
proof end;
end;

theorem Th8: :: WAYBEL30:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty reflexive RelStr holds sigma T c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
proof end;

theorem Th9: :: WAYBEL30:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Lawson TopLattice holds lambda N = the topology of N
proof end;

theorem Th10: :: WAYBEL30:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Lawson TopLattice holds sigma N c= lambda N
proof end;

theorem :: WAYBEL30:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M, N being complete LATTICE st RelStr(# the carrier of M,the InternalRel of M #) = RelStr(# the carrier of N,the InternalRel of N #) holds
lambda M = lambda N
proof end;

theorem Th12: :: WAYBEL30:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Lawson TopLattice
for X being Subset of N holds
( X in lambda N iff X is open )
proof end;

registration
cluster non empty TopSpace-like reflexive trivial -> non empty reflexive Scott TopRelStr ;
coherence
for b1 being non empty reflexive TopRelStr st b1 is trivial & b1 is TopSpace-like holds
b1 is Scott
proof end;
end;

registration
cluster complete trivial -> complete Lawson TopRelStr ;
coherence
for b1 being complete TopLattice st b1 is trivial holds
b1 is Lawson
proof end;
end;

registration
cluster complete lower-bounded meet-continuous strict Scott continuous TopRelStr ;
existence
ex b1 being complete TopLattice st
( b1 is strict & b1 is continuous & b1 is lower-bounded & b1 is meet-continuous & b1 is Scott )
proof end;
end;

registration
cluster complete compact Hausdorff strict Lawson continuous TopRelStr ;
existence
ex b1 being complete TopLattice st
( b1 is strict & b1 is continuous & b1 is compact & b1 is being_T2 & b1 is Lawson )
proof end;
end;

scheme :: WAYBEL30:sch 1
EmptySch{ F1() -> Scott TopLattice, F2() -> set , F3( set ) -> set } :
{ F3(w) where w is Element of F1() : w in {} } = {}
proof end;

theorem Th13: :: WAYBEL30:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being meet-continuous LATTICE
for A being Subset of N st A has_the_property_(S) holds
uparrow A has_the_property_(S)
proof end;

registration
let N be meet-continuous LATTICE;
let A be property(S) Subset of N;
cluster uparrow A -> property(S) ;
coherence
uparrow A is property(S)
by Th13;
end;

theorem Th14: :: WAYBEL30:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice
for S being Scott TopAugmentation of N
for A being Subset of N st A in lambda N holds
uparrow A in sigma S
proof end;

theorem Th15: :: WAYBEL30:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice
for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J & A is open holds
uparrow J is open
proof end;

theorem Th16: :: WAYBEL30:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice
for S being Scott TopAugmentation of N
for x being Point of S
for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
proof end;

theorem Th17: :: WAYBEL30:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice
for S being Scott TopAugmentation of N
for X being upper Subset of N
for Y being Subset of S st X = Y holds
Int X = Int Y
proof end;

theorem :: WAYBEL30:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice
for S being Scott TopAugmentation of N
for X being lower Subset of N
for Y being Subset of S st X = Y holds
Cl X = Cl Y
proof end;

theorem Th19: :: WAYBEL30:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M, N being complete LATTICE
for LM being correct Lawson TopAugmentation of M
for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
the topology of [:LM,LN:] = lambda [:M,N:]
proof end;

theorem Th20: :: WAYBEL30:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M, N being complete LATTICE
for P being correct Lawson TopAugmentation of [:M,N:]
for Q being correct Lawson TopAugmentation of M
for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
TopStruct(# the carrier of P,the topology of P #) = [:Q,R:]
proof end;

theorem Th21: :: WAYBEL30:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice
for x being Element of N holds x "/\" is continuous
proof end;

registration
let N be complete meet-continuous Lawson TopLattice;
let x be Element of N;
cluster x "/\" -> continuous ;
coherence
x "/\" is continuous
by Th21;
end;

theorem Th22: :: WAYBEL30:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice st InclPoset (sigma N) is continuous holds
N is topological_semilattice
proof end;

Lm3: now
let S, T, x1, x2 be set ; :: thesis: ( x1 in S & x2 in T implies <:(pr2 S,T),(pr1 S,T):> . [x1,x2] = [x2,x1] )
assume A1: ( x1 in S & x2 in T ) ; :: thesis: <:(pr2 S,T),(pr1 S,T):> . [x1,x2] = [x2,x1]
A2: dom <:(pr2 S,T),(pr1 S,T):> = (dom (pr2 S,T)) /\ (dom (pr1 S,T)) by FUNCT_3:def 8
.= (dom (pr2 S,T)) /\ [:S,T:] by FUNCT_3:def 5
.= [:S,T:] /\ [:S,T:] by FUNCT_3:def 6
.= [:S,T:] ;
[x1,x2] in [:S,T:] by A1, ZFMISC_1:106;
hence <:(pr2 S,T),(pr1 S,T):> . [x1,x2] = [((pr2 S,T) . [x1,x2]),((pr1 S,T) . [x1,x2])] by A2, FUNCT_3:def 8
.= [x2,((pr1 S,T) . [x1,x2])] by A1, FUNCT_3:def 6
.= [x2,x1] by A1, FUNCT_3:def 5 ;
:: thesis: verum
end;

theorem :: WAYBEL30:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice st InclPoset (sigma N) is continuous holds
( N is being_T2 iff for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed )
proof end;

definition
let N be non empty reflexive RelStr ;
let X be Subset of N;
func X ^0 -> Subset of N equals :: WAYBEL30:def 1
{ u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D
}
;
coherence
{ u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D
}
is Subset of N
proof end;
end;

:: deftheorem defines ^0 WAYBEL30:def 1 :
for N being non empty reflexive RelStr
for X being Subset of N holds X ^0 = { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D
}
;

registration
let N be non empty reflexive antisymmetric RelStr ;
let X be empty Subset of N;
cluster X ^0 -> empty ;
coherence
X ^0 is empty
proof end;
end;

theorem :: WAYBEL30:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty reflexive RelStr
for A, J being Subset of N st A c= J holds
A ^0 c= J ^0
proof end;

theorem Th25: :: WAYBEL30:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty reflexive RelStr
for x being Element of N holds (uparrow x) ^0 = wayabove x
proof end;

theorem Th26: :: WAYBEL30:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Scott TopLattice
for X being upper Subset of N holds Int X c= X ^0
proof end;

theorem Th27: :: WAYBEL30:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty reflexive RelStr
for X, Y being Subset of N holds (X ^0 ) \/ (Y ^0 ) c= (X \/ Y) ^0
proof end;

theorem Th28: :: WAYBEL30:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being meet-continuous LATTICE
for X, Y being upper Subset of N holds (X ^0 ) \/ (Y ^0 ) = (X \/ Y) ^0
proof end;

theorem Th29: :: WAYBEL30:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being meet-continuous Scott TopLattice
for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }
proof end;

theorem Th30: :: WAYBEL30:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Lawson TopLattice holds
( N is continuous iff ( N is meet-continuous & N is being_T2 ) )
proof end;

registration
cluster complete Lawson continuous -> complete Hausdorff TopRelStr ;
coherence
for b1 being complete TopLattice st b1 is continuous & b1 is Lawson holds
b1 is being_T2
by Th30;
cluster complete meet-continuous Hausdorff Lawson -> complete continuous TopRelStr ;
coherence
for b1 being complete TopLattice st b1 is meet-continuous & b1 is Lawson & b1 is being_T2 holds
b1 is continuous
by Th30;
end;

definition
let N be non empty TopRelStr ;
attr N is with_small_semilattices means :: WAYBEL30:def 2
for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting;
attr N is with_compact_semilattices means :: WAYBEL30:def 3
for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
( subrelstr A is meet-inheriting & A is compact );
attr N is with_open_semilattices means :Def4: :: WAYBEL30:def 4
for x being Point of N ex J being Basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting;
end;

:: deftheorem defines with_small_semilattices WAYBEL30:def 2 :
for N being non empty TopRelStr holds
( N is with_small_semilattices iff for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting );

:: deftheorem defines with_compact_semilattices WAYBEL30:def 3 :
for N being non empty TopRelStr holds
( N is with_compact_semilattices iff for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
( subrelstr A is meet-inheriting & A is compact ) );

:: deftheorem Def4 defines with_open_semilattices WAYBEL30:def 4 :
for N being non empty TopRelStr holds
( N is with_open_semilattices iff for x being Point of N ex J being Basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting );

registration
cluster non empty TopSpace-like with_open_semilattices -> non empty TopSpace-like with_small_semilattices TopRelStr ;
coherence
for b1 being non empty TopSpace-like TopRelStr st b1 is with_open_semilattices holds
b1 is with_small_semilattices
proof end;
cluster non empty TopSpace-like with_compact_semilattices -> non empty TopSpace-like with_small_semilattices TopRelStr ;
coherence
for b1 being non empty TopSpace-like TopRelStr st b1 is with_compact_semilattices holds
b1 is with_small_semilattices
proof end;
cluster non empty anti-discrete -> non empty with_small_semilattices with_open_semilattices TopRelStr ;
coherence
for b1 being non empty TopRelStr st b1 is anti-discrete holds
( b1 is with_small_semilattices & b1 is with_open_semilattices )
proof end;
cluster non empty TopSpace-like reflexive trivial -> non empty with_compact_semilattices TopRelStr ;
coherence
for b1 being non empty TopRelStr st b1 is reflexive & b1 is trivial & b1 is TopSpace-like holds
b1 is with_compact_semilattices
proof end;
end;

registration
cluster Hausdorff strict lower Lawson Scott trivial with_small_semilattices with_compact_semilattices with_open_semilattices TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is strict & b1 is trivial & b1 is lower )
proof end;
end;

theorem Th31: :: WAYBEL30:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being with_infima topological_semilattice TopPoset
for C being Subset of N st subrelstr C is meet-inheriting holds
subrelstr (Cl C) is meet-inheriting
proof end;

theorem Th32: :: WAYBEL30:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice
for S being Scott TopAugmentation of N holds
( ( for x being Point of S ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S ) iff N is with_open_semilattices )
proof end;

theorem Th33: :: WAYBEL30:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Lawson TopLattice
for S being Scott TopAugmentation of N
for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
proof end;

theorem Th34: :: WAYBEL30:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice
for S being Scott TopAugmentation of N
for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
proof end;

theorem Th35: :: WAYBEL30:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice holds
( N is continuous iff ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) )
proof end;

registration
cluster complete Lawson continuous -> complete Lawson with_small_semilattices with_open_semilattices TopRelStr ;
coherence
for b1 being complete Lawson TopLattice st b1 is continuous holds
b1 is with_open_semilattices
proof end;
end;

registration
let N be complete Lawson continuous TopLattice;
cluster InclPoset (sigma N) -> complete continuous non trivial ;
coherence
InclPoset (sigma N) is continuous
by Th35;
end;

theorem :: WAYBEL30:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Lawson continuous TopLattice holds
( N is compact & N is being_T2 & N is topological_semilattice & N is with_open_semilattices )
proof end;

theorem :: WAYBEL30:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete Hausdorff Lawson topological_semilattice with_open_semilattices TopLattice holds N is with_compact_semilattices
proof end;

theorem :: WAYBEL30:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Hausdorff Lawson TopLattice
for x being Element of N holds x = "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N
proof end;

theorem :: WAYBEL30:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice holds
( N is continuous iff for x being Element of N holds x = "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N )
proof end;

theorem Th40: :: WAYBEL30:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being complete meet-continuous Lawson TopLattice holds
( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) )
proof end;

registration
let N be complete algebraic meet-continuous Lawson TopLattice;
cluster InclPoset (sigma N) -> complete algebraic continuous non trivial ;
coherence
InclPoset (sigma N) is algebraic
by Th40;
end;