:: More on the Lattice of Congruences in a Many Sorted Algebra
:: by Robert Milewski
::
:: Received March 6, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem Th1: :: MSUALG_8:1
theorem Th2: :: MSUALG_8:2
theorem :: MSUALG_8:3
theorem :: MSUALG_8:4
theorem Th5: :: MSUALG_8:5
theorem Th6: :: MSUALG_8:6
theorem Th7: :: MSUALG_8:7
theorem Th8: :: MSUALG_8:8
theorem Th9: :: MSUALG_8:9
theorem Th10: :: MSUALG_8:10
theorem Th11: :: MSUALG_8:11
:: deftheorem defines CongrCl MSUALG_8:def 1 :
:: deftheorem defines CongrCl MSUALG_8:def 2 :
theorem :: MSUALG_8:12
theorem :: MSUALG_8:13
theorem :: MSUALG_8:14
theorem :: MSUALG_8:15
theorem Th16: :: MSUALG_8:16
:: deftheorem Def3 defines EqRelSet MSUALG_8:def 3 :
theorem Th17: :: MSUALG_8:17
theorem Th18: :: MSUALG_8:18
theorem Th19: :: MSUALG_8:19
theorem Th20: :: MSUALG_8:20