:: Properties of First and Second Order Cutting of Binary Relations
:: by Krzysztof Retel
::
:: Received April 25, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: RELSET_2:1
theorem Th2: :: RELSET_2:2
theorem Th3: :: RELSET_2:3
theorem Th4: :: RELSET_2:4
theorem :: RELSET_2:5
theorem Th6: :: RELSET_2:6
theorem :: RELSET_2:7
theorem :: RELSET_2:8
definition
canceled;
end;
:: deftheorem RELSET_2:def 1 :
canceled;
theorem Th9: :: RELSET_2:9
theorem Th10: :: RELSET_2:10
theorem Th11: :: RELSET_2:11
theorem :: RELSET_2:12
theorem :: RELSET_2:13
theorem :: RELSET_2:14
theorem Th15: :: RELSET_2:15
theorem :: RELSET_2:16
theorem :: RELSET_2:17
theorem :: RELSET_2:18
:: deftheorem RELSET_2:def 2 :
canceled;
:: deftheorem Def3 defines .: RELSET_2:def 3 :
theorem Th19: :: RELSET_2:19
theorem Th20: :: RELSET_2:20
theorem Th21: :: RELSET_2:21
theorem :: RELSET_2:22
:: deftheorem defines .:^ RELSET_2:def 4 :
theorem Th23: :: RELSET_2:23
theorem Th24: :: RELSET_2:24
theorem Th25: :: RELSET_2:25
theorem :: RELSET_2:26
theorem :: RELSET_2:27
theorem :: RELSET_2:28
theorem Th29: :: RELSET_2:29
theorem :: RELSET_2:30
canceled;
theorem :: RELSET_2:31
theorem Th32: :: RELSET_2:32
theorem :: RELSET_2:33
theorem :: RELSET_2:34
theorem :: RELSET_2:35
theorem :: RELSET_2:36
theorem Th37: :: RELSET_2:37
theorem Th38: :: RELSET_2:38
theorem :: RELSET_2:39
theorem :: RELSET_2:40
theorem :: RELSET_2:41
theorem Th42: :: RELSET_2:42
theorem :: RELSET_2:43
theorem Th44: :: RELSET_2:44
theorem Th45: :: RELSET_2:45
theorem Th46: :: RELSET_2:46
theorem Th47: :: RELSET_2:47
theorem Th48: :: RELSET_2:48
theorem Th49: :: RELSET_2:49
theorem Th50: :: RELSET_2:50
theorem Th51: :: RELSET_2:51
theorem :: RELSET_2:52
theorem :: RELSET_2:53
theorem :: RELSET_2:54
theorem :: RELSET_2:55
theorem :: RELSET_2:56
theorem :: RELSET_2:57
theorem :: RELSET_2:58
theorem :: RELSET_2:59
theorem Th60: :: RELSET_2:60
theorem Th61: :: RELSET_2:61
theorem :: RELSET_2:62
theorem :: RELSET_2:63
theorem :: RELSET_2:64
theorem :: RELSET_2:65