:: Completely-Irreducible Elements
:: by Robert Milewski
::
:: Received February 9, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem Th1: :: WAYBEL16:1
theorem :: WAYBEL16:2
theorem Th3: :: WAYBEL16:3
theorem :: WAYBEL16:4
theorem Th5: :: WAYBEL16:5
theorem :: WAYBEL16:6
theorem Th7: :: WAYBEL16:7
theorem :: WAYBEL16:8
:: deftheorem defines CLHomomorphism WAYBEL16:def 1 :
:: deftheorem defines is_FG_set WAYBEL16:def 2 :
theorem Th9: :: WAYBEL16:9
theorem :: WAYBEL16:10
theorem Th11: :: WAYBEL16:11
theorem Th12: :: WAYBEL16:12
theorem :: WAYBEL16:13
theorem :: WAYBEL16:14
theorem :: WAYBEL16:15
theorem :: WAYBEL16:16
theorem :: WAYBEL16:17
theorem Th18: :: WAYBEL16:18
:: deftheorem Def3 defines completely-irreducible WAYBEL16:def 3 :
theorem Th19: :: WAYBEL16:19
:: deftheorem Def4 defines Irr WAYBEL16:def 4 :
theorem Th20: :: WAYBEL16:20
theorem Th21: :: WAYBEL16:21
theorem Th22: :: WAYBEL16:22
theorem Th23: :: WAYBEL16:23
theorem Th24: :: WAYBEL16:24
theorem Th25: :: WAYBEL16:25
theorem Th26: :: WAYBEL16:26
theorem Th27: :: WAYBEL16:27
theorem Th28: :: WAYBEL16:28
theorem Th29: :: WAYBEL16:29
theorem :: WAYBEL16:30
theorem Th31: :: WAYBEL16:31
theorem Th32: :: WAYBEL16:32
theorem :: WAYBEL16:33
theorem Th34: :: WAYBEL16:34
theorem Th35: :: WAYBEL16:35
theorem :: WAYBEL16:36