:: Algebraic Operation on Subsets of Many Sorted Sets
:: by Agnieszka Julia Marasik
::
:: Received June 23, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem Th1: :: CLOSURE3:1
theorem :: CLOSURE3:2
theorem Th3: :: CLOSURE3:3
theorem :: CLOSURE3:4
canceled;
theorem :: CLOSURE3:5
:: deftheorem CLOSURE3:def 1 :
canceled;
:: deftheorem CLOSURE3:def 2 :
canceled;
:: deftheorem Def3 defines supp CLOSURE3:def 3 :
theorem :: CLOSURE3:6
theorem :: CLOSURE3:7
theorem :: CLOSURE3:8
theorem Th9: :: CLOSURE3:9
:: deftheorem Def4 defines MSUnion CLOSURE3:def 4 :
theorem :: CLOSURE3:10
theorem :: CLOSURE3:11
theorem :: CLOSURE3:12
theorem :: CLOSURE3:13
theorem :: CLOSURE3:14
:: deftheorem defines algebraic CLOSURE3:def 5 :
:: deftheorem defines algebraic CLOSURE3:def 6 :
:: deftheorem Def7 defines SubAlgCl CLOSURE3:def 7 :
theorem :: CLOSURE3:15
canceled;
theorem Th16: :: CLOSURE3:16