:: Closure Operators and Subalgebras
:: by Grzegorz Bancerek
::
:: Received January 15, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem Th1: :: WAYBEL10:1
theorem :: WAYBEL10:2
canceled;
theorem Th3: :: WAYBEL10:3
theorem Th4: :: WAYBEL10:4
theorem :: WAYBEL10:5
theorem Th6: :: WAYBEL10:6
:: deftheorem Def1 defines | WAYBEL10:def 1 :
theorem Th7: :: WAYBEL10:7
theorem Th8: :: WAYBEL10:8
theorem Th9: :: WAYBEL10:9
theorem Th10: :: WAYBEL10:10
:: deftheorem Def2 defines ClOpers WAYBEL10:def 2 :
theorem Th11: :: WAYBEL10:11
theorem Th12: :: WAYBEL10:12
theorem Th13: :: WAYBEL10:13
theorem Th14: :: WAYBEL10:14
theorem Th15: :: WAYBEL10:15
:: deftheorem Def3 defines Sub WAYBEL10:def 3 :
theorem Th16: :: WAYBEL10:16
:: deftheorem Def4 defines ClosureSystems WAYBEL10:def 4 :
theorem Th17: :: WAYBEL10:17
theorem Th18: :: WAYBEL10:18
:: deftheorem Def5 defines ClImageMap WAYBEL10:def 5 :
:: deftheorem Def6 defines closure_op WAYBEL10:def 6 :
theorem Th19: :: WAYBEL10:19
theorem Th20: :: WAYBEL10:20
theorem Th21: :: WAYBEL10:21
theorem Th22: :: WAYBEL10:22
theorem :: WAYBEL10:23
theorem Th24: :: WAYBEL10:24
theorem Th25: :: WAYBEL10:25
theorem :: WAYBEL10:26
:: deftheorem Def7 defines DsupClOpers WAYBEL10:def 7 :
theorem Th27: :: WAYBEL10:27
:: deftheorem Def8 defines Subalgebras WAYBEL10:def 8 :
theorem Th28: :: WAYBEL10:28
theorem Th29: :: WAYBEL10:29
theorem :: WAYBEL10:30