:: On the Lattice of Subgroups of a Group
:: by Janusz Ganczarski
::
:: Received May 23, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem Th1: :: LATSUBGR:1
theorem Th2: :: LATSUBGR:2
theorem Th3: :: LATSUBGR:3
theorem Th4: :: LATSUBGR:4
theorem Th5: :: LATSUBGR:5
theorem :: LATSUBGR:6
theorem :: LATSUBGR:7
theorem :: LATSUBGR:8
canceled;
theorem :: LATSUBGR:9
canceled;
theorem :: LATSUBGR:10
theorem :: LATSUBGR:11
theorem :: LATSUBGR:12
theorem :: LATSUBGR:13
theorem Th14: :: LATSUBGR:14
:: deftheorem Def1 defines carr LATSUBGR:def 1 :
theorem :: LATSUBGR:15
canceled;
theorem :: LATSUBGR:16
canceled;
theorem :: LATSUBGR:17
canceled;
theorem Th18: :: LATSUBGR:18
theorem :: LATSUBGR:19
theorem :: LATSUBGR:20
theorem :: LATSUBGR:21
theorem :: LATSUBGR:22
theorem Th23: :: LATSUBGR:23
theorem :: LATSUBGR:24
:: deftheorem Def2 defines meet LATSUBGR:def 2 :
theorem :: LATSUBGR:25
theorem :: LATSUBGR:26
theorem Th27: :: LATSUBGR:27
theorem Th28: :: LATSUBGR:28
theorem Th29: :: LATSUBGR:29
theorem Th30: :: LATSUBGR:30
theorem :: LATSUBGR:31
theorem :: LATSUBGR:32
:: deftheorem Def3 defines FuncLatt LATSUBGR:def 3 :
theorem :: LATSUBGR:33
theorem :: LATSUBGR:34
theorem :: LATSUBGR:35
theorem Th36: :: LATSUBGR:36
theorem Th37: :: LATSUBGR:37
theorem :: LATSUBGR:38