:: On the Lattice of Subalgebras of a Universal Algebra
:: by Miros{\l}aw Jan Paszek
::
:: Received May 23, 1995
:: Copyright (c) 1995 Association of Mizar Users
:: deftheorem Def1 defines SubAlgebra-Family UNIALG_3:def 1 :
:: deftheorem Def2 defines carr UNIALG_3:def 2 :
:: deftheorem Def3 defines Carr UNIALG_3:def 3 :
theorem Th1: :: UNIALG_3:1
theorem :: UNIALG_3:2
theorem Th3: :: UNIALG_3:3
theorem :: UNIALG_3:4
theorem :: UNIALG_3:5
theorem Th6: :: UNIALG_3:6
theorem :: UNIALG_3:7
:: deftheorem Def4 defines Carr UNIALG_3:def 4 :
theorem :: UNIALG_3:8
theorem Th9: :: UNIALG_3:9
theorem :: UNIALG_3:10
theorem Th11: :: UNIALG_3:11
theorem Th12: :: UNIALG_3:12
theorem :: UNIALG_3:13
theorem Th14: :: UNIALG_3:14
:: deftheorem Def5 defines meet UNIALG_3:def 5 :
theorem :: UNIALG_3:15
canceled;
theorem :: UNIALG_3:16
canceled;
theorem Th17: :: UNIALG_3:17
theorem :: UNIALG_3:18
theorem Th19: :: UNIALG_3:19
theorem Th20: :: UNIALG_3:20
theorem :: UNIALG_3:21
theorem Th22: :: UNIALG_3:22
theorem Th23: :: UNIALG_3:23
theorem :: UNIALG_3:24
theorem :: UNIALG_3:25
:: deftheorem Def6 defines FuncLatt UNIALG_3:def 6 :
theorem :: UNIALG_3:26