:: Many-Argument Relations
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines relation-like MARGREL1:def 1 :
theorem :: MARGREL1:1
canceled;
theorem :: MARGREL1:2
canceled;
theorem :: MARGREL1:3
canceled;
theorem :: MARGREL1:4
canceled;
theorem :: MARGREL1:5
canceled;
theorem :: MARGREL1:6
canceled;
theorem :: MARGREL1:7
theorem :: MARGREL1:8
:: deftheorem defines = MARGREL1:def 2 :
theorem Th9: :: MARGREL1:9
:: deftheorem MARGREL1:def 3 :
canceled;
:: deftheorem defines the_arity_of MARGREL1:def 4 :
:: deftheorem defines relation_length MARGREL1:def 5 :
:: deftheorem defines relation MARGREL1:def 6 :
theorem :: MARGREL1:10
canceled;
theorem :: MARGREL1:11
canceled;
theorem :: MARGREL1:12
canceled;
theorem :: MARGREL1:13
canceled;
theorem :: MARGREL1:14
canceled;
theorem :: MARGREL1:15
canceled;
theorem :: MARGREL1:16
canceled;
theorem :: MARGREL1:17
canceled;
theorem :: MARGREL1:18
canceled;
theorem :: MARGREL1:19
canceled;
theorem Th20: :: MARGREL1:20
theorem Th21: :: MARGREL1:21
:: deftheorem defines relation MARGREL1:def 7 :
:: deftheorem Def8 defines relations_on MARGREL1:def 8 :
theorem :: MARGREL1:22
canceled;
theorem :: MARGREL1:23
canceled;
theorem :: MARGREL1:24
canceled;
theorem :: MARGREL1:25
canceled;
theorem :: MARGREL1:26
theorem :: MARGREL1:27
theorem :: MARGREL1:28
:: deftheorem Def9 defines = MARGREL1:def 9 :
:: deftheorem Def10 defines empty_rel MARGREL1:def 10 :
theorem :: MARGREL1:29
canceled;
theorem :: MARGREL1:30
canceled;
theorem :: MARGREL1:31
canceled;
theorem :: MARGREL1:32
:: deftheorem defines the_arity_of MARGREL1:def 11 :
:: deftheorem defines BOOLEAN MARGREL1:def 12 :
:: deftheorem Def13 defines boolean MARGREL1:def 13 :
:: deftheorem defines 'not' MARGREL1:def 14 :
:: deftheorem defines '&' MARGREL1:def 15 :
theorem :: MARGREL1:33
canceled;
theorem :: MARGREL1:34
canceled;
theorem :: MARGREL1:35
canceled;
theorem :: MARGREL1:36
canceled;
theorem :: MARGREL1:37
canceled;
theorem :: MARGREL1:38
canceled;
theorem :: MARGREL1:39
canceled;
theorem :: MARGREL1:40
theorem :: MARGREL1:41
theorem :: MARGREL1:42
canceled;
theorem :: MARGREL1:43
canceled;
theorem :: MARGREL1:44
canceled;
theorem :: MARGREL1:45
theorem :: MARGREL1:46
canceled;
theorem :: MARGREL1:47
canceled;
theorem :: MARGREL1:48
canceled;
theorem :: MARGREL1:49
theorem :: MARGREL1:50
theorem :: MARGREL1:51
theorem :: MARGREL1:52
:: deftheorem Def16 defines ALL MARGREL1:def 16 :
theorem :: MARGREL1:53
:: deftheorem Def17 defines boolean-valued MARGREL1:def 17 :
:: deftheorem Def18 defines 'not' MARGREL1:def 18 :
:: deftheorem Def19 defines '&' MARGREL1:def 19 :
:: deftheorem defines 'not' MARGREL1:def 20 :
:: deftheorem defines '&' MARGREL1:def 21 :