:: Certain Facts about Families of Subsets of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received October 27, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem :: MSSUBFAM:1
theorem :: MSSUBFAM:2
theorem :: MSSUBFAM:3
theorem :: MSSUBFAM:4
theorem :: MSSUBFAM:5
theorem :: MSSUBFAM:6
theorem :: MSSUBFAM:7
theorem :: MSSUBFAM:8
theorem :: MSSUBFAM:9
theorem :: MSSUBFAM:10
theorem :: MSSUBFAM:11
theorem :: MSSUBFAM:12
theorem Th13: :: MSSUBFAM:13
theorem Th14: :: MSSUBFAM:14
theorem :: MSSUBFAM:15
theorem :: MSSUBFAM:16
theorem :: MSSUBFAM:17
theorem Th18: :: MSSUBFAM:18
theorem :: MSSUBFAM:19
theorem :: MSSUBFAM:20
theorem Th21: :: MSSUBFAM:21
theorem :: MSSUBFAM:22
theorem :: MSSUBFAM:23
theorem :: MSSUBFAM:24
theorem :: MSSUBFAM:25
theorem :: MSSUBFAM:26
theorem :: MSSUBFAM:27
theorem :: MSSUBFAM:28
theorem :: MSSUBFAM:29
theorem :: MSSUBFAM:30
theorem :: MSSUBFAM:31
theorem Th32: :: MSSUBFAM:32
theorem Th33: :: MSSUBFAM:33
theorem Th34: :: MSSUBFAM:34
theorem :: MSSUBFAM:35
theorem Th36: :: MSSUBFAM:36
theorem :: MSSUBFAM:37
theorem Th38: :: MSSUBFAM:38
theorem Th39: :: MSSUBFAM:39
theorem Th40: :: MSSUBFAM:40
:: deftheorem MSSUBFAM:def 1 :
canceled;
:: deftheorem Def2 defines meet MSSUBFAM:def 2 :
theorem Th41: :: MSSUBFAM:41
theorem :: MSSUBFAM:42
theorem :: MSSUBFAM:43
theorem :: MSSUBFAM:44
theorem :: MSSUBFAM:45
theorem :: MSSUBFAM:46
theorem :: MSSUBFAM:47
theorem :: MSSUBFAM:48
theorem :: MSSUBFAM:49
theorem :: MSSUBFAM:50
theorem Th51: :: MSSUBFAM:51
theorem :: MSSUBFAM:52
theorem :: MSSUBFAM:53
:: deftheorem defines additive MSSUBFAM:def 3 :
:: deftheorem Def4 defines absolutely-additive MSSUBFAM:def 4 :
:: deftheorem defines multiplicative MSSUBFAM:def 5 :
:: deftheorem Def6 defines absolutely-multiplicative MSSUBFAM:def 6 :
:: deftheorem Def7 defines properly-upper-bound MSSUBFAM:def 7 :
:: deftheorem Def8 defines properly-lower-bound MSSUBFAM:def 8 :
Lm1:
for I being set
for M being ManySortedSet of I holds
( bool M is additive & bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound )