:: The {H}all {M}arriage {T}heorem
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received May 11, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: HALLMAR1:1
theorem Th2: :: HALLMAR1:2
:: deftheorem Def1 defines union HALLMAR1:def 1 :
theorem Th3: :: HALLMAR1:3
theorem :: HALLMAR1:4
theorem Th5: :: HALLMAR1:5
theorem Th6: :: HALLMAR1:6
theorem Th7: :: HALLMAR1:7
theorem Th8: :: HALLMAR1:8
theorem Th9: :: HALLMAR1:9
theorem Th10: :: HALLMAR1:10
:: deftheorem Def2 defines Cut HALLMAR1:def 2 :
theorem Th11: :: HALLMAR1:11
theorem Th12: :: HALLMAR1:12
theorem Th13: :: HALLMAR1:13
theorem Th14: :: HALLMAR1:14
:: deftheorem Def3 defines is_a_system_of_different_representatives_of HALLMAR1:def 3 :
:: deftheorem Def4 defines Hall HALLMAR1:def 4 :
theorem Th15: :: HALLMAR1:15
theorem Th16: :: HALLMAR1:16
theorem Th17: :: HALLMAR1:17
theorem Th18: :: HALLMAR1:18
:: deftheorem Def5 defines Reduction HALLMAR1:def 5 :
:: deftheorem Def6 defines Reduction HALLMAR1:def 6 :
:: deftheorem Def7 defines Singlification HALLMAR1:def 7 :
theorem Th19: :: HALLMAR1:19
theorem Th20: :: HALLMAR1:20
theorem Th21: :: HALLMAR1:21
theorem Th22: :: HALLMAR1:22
theorem :: HALLMAR1:23
theorem Th24: :: HALLMAR1:24
theorem :: HALLMAR1:25
theorem Th26: :: HALLMAR1:26
:: deftheorem Def8 defines Singlification HALLMAR1:def 8 :
theorem Th27: :: HALLMAR1:27
theorem Th28: :: HALLMAR1:28
theorem Th29: :: HALLMAR1:29
theorem Th30: :: HALLMAR1:30
theorem Th31: :: HALLMAR1:31
theorem :: HALLMAR1:32