:: The Lawson Topology
:: by Grzegorz Bancerek
::
:: Received June 21, 1998
:: Copyright (c) 1998 Association of Mizar Users
:: deftheorem Def1 defines lower WAYBEL19:def 1 :
theorem Th1: :: WAYBEL19:1
theorem Th2: :: WAYBEL19:2
:: deftheorem Def2 defines omega WAYBEL19:def 2 :
theorem Th3: :: WAYBEL19:3
theorem Th4: :: WAYBEL19:4
theorem Th5: :: WAYBEL19:5
theorem Th6: :: WAYBEL19:6
theorem Th7: :: WAYBEL19:7
theorem Th8: :: WAYBEL19:8
theorem Th9: :: WAYBEL19:9
theorem Th10: :: WAYBEL19:10
theorem Th11: :: WAYBEL19:11
theorem :: WAYBEL19:12
theorem :: WAYBEL19:13
theorem Th14: :: WAYBEL19:14
theorem Th15: :: WAYBEL19:15
theorem :: WAYBEL19:16
theorem :: WAYBEL19:17
theorem :: WAYBEL19:18
theorem Th19: :: WAYBEL19:19
theorem Th20: :: WAYBEL19:20
theorem Th21: :: WAYBEL19:21
theorem Th22: :: WAYBEL19:22
theorem Th23: :: WAYBEL19:23
theorem :: WAYBEL19:24
theorem Th25: :: WAYBEL19:25
theorem Th26: :: WAYBEL19:26
theorem Th27: :: WAYBEL19:27
theorem Th28: :: WAYBEL19:28
:: deftheorem Def3 defines Lawson WAYBEL19:def 3 :
theorem Th29: :: WAYBEL19:29
theorem Th30: :: WAYBEL19:30
theorem :: WAYBEL19:31
theorem :: WAYBEL19:32
:: deftheorem Def4 defines lambda WAYBEL19:def 4 :
theorem Th33: :: WAYBEL19:33
theorem :: WAYBEL19:34
Lm2:
for T being LATTICE
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A is property(S) ) holds
union F is property(S)
Lm3:
for T being LATTICE
for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds
A1 /\ A2 is property(S)
Lm4:
for T being LATTICE holds [#] T is property(S)
theorem Th35: :: WAYBEL19:35
theorem Th36: :: WAYBEL19:36
theorem Th37: :: WAYBEL19:37
theorem Th38: :: WAYBEL19:38
theorem Th39: :: WAYBEL19:39
theorem Th40: :: WAYBEL19:40
theorem :: WAYBEL19:41
theorem :: WAYBEL19:42
theorem :: WAYBEL19:43