begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
Lm3:
now
let S,
T,
x1,
x2 be
set ;
( x1 in S & x2 in T implies <:(pr2 S,T),(pr1 S,T):> . [x1,x2] = [x2,x1] )assume that A1:
x1 in S
and A2:
x2 in T
;
<:(pr2 S,T),(pr1 S,T):> . [x1,x2] = [x2,x1]A3:
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, A2, ZFMISC_1:106;
hence <:(pr2 S,T),(pr1 S,T):> . [x1,x2] =
[((pr2 S,T) . x1,x2),((pr1 S,T) . x1,x2)]
by A3, FUNCT_3:def 8
.=
[x2,((pr1 S,T) . x1,x2)]
by A1, A2, FUNCT_3:def 6
.=
[x2,x1]
by A1, A2, FUNCT_3:def 5
;
verum
end;
theorem
:: 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 } ;
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
:: 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 );
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem
theorem
theorem
theorem Th40: