:: WAYBEL12 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
Lm1:
for L being non empty RelStr
for f being Function of NAT ,the carrier of L
for n being Nat holds { (f . k) where k is Nat : k <= n } is non empty finite Subset of L
:: deftheorem defines closed WAYBEL12:def 1 :
:: deftheorem Def2 defines dense WAYBEL12:def 2 :
theorem :: WAYBEL12:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th2: :: WAYBEL12:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th3: :: WAYBEL12:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th4: :: WAYBEL12:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm2:
for S being 1-sorted
for X, Y being Subset of S holds (X \/ Y) ` = (X ` ) /\ (Y ` )
by SUBSET_1:29;
Lm3:
for S being 1-sorted
for X, Y being Subset of S holds (X /\ Y) ` = (X ` ) \/ (Y ` )
by SUBSET_1:30;
theorem :: WAYBEL12:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: WAYBEL12:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: WAYBEL12:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th8: :: WAYBEL12:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: WAYBEL12:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: WAYBEL12:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: WAYBEL12:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: WAYBEL12:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th18: :: WAYBEL12:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: WAYBEL12:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th21: :: WAYBEL12:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th23: :: WAYBEL12:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th25: :: WAYBEL12:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm4:
for L being non empty RelStr
for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is Subset of L
theorem Th27: :: WAYBEL12:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th28: :: WAYBEL12:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th29: :: WAYBEL12:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th30: :: WAYBEL12:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th31: :: WAYBEL12:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL12:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm5:
for L being Semilattice
for F being Filter of L holds F = uparrow (fininfs F)
:: deftheorem Def3 defines GeneratorSet WAYBEL12:def 3 :
Lm6:
for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F holds G c= F
theorem Th33: :: WAYBEL12:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th34: :: WAYBEL12:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th35: :: WAYBEL12:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th36: :: WAYBEL12:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th37: :: WAYBEL12:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th38: :: WAYBEL12:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th39: :: WAYBEL12:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th40: :: WAYBEL12:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def4 defines dense WAYBEL12:def 4 :
theorem :: WAYBEL12:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def5 defines dense WAYBEL12:def 5 :
theorem Th42: :: WAYBEL12:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th43: :: WAYBEL12:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th44: :: WAYBEL12:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th45: :: WAYBEL12:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th46: :: WAYBEL12:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th47: :: WAYBEL12:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines Baire WAYBEL12:def 6 :
theorem :: WAYBEL12:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) 