:: The Contraction Lemma
:: by Grzegorz Bancerek
::
:: Received April 14, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines Collapse ZF_COLLA:def 1 :
theorem Th1: :: ZF_COLLA:1
theorem :: ZF_COLLA:2
theorem :: ZF_COLLA:3
theorem Th4: :: ZF_COLLA:4
theorem Th5: :: ZF_COLLA:5
theorem Th6: :: ZF_COLLA:6
theorem Th7: :: ZF_COLLA:7
theorem Th8: :: ZF_COLLA:8
theorem Th9: :: ZF_COLLA:9
:: deftheorem defines is_epsilon-isomorphism_of ZF_COLLA:def 2 :
:: deftheorem defines are_epsilon-isomorphic ZF_COLLA:def 3 :
theorem :: ZF_COLLA:10
canceled;
theorem :: ZF_COLLA:11
canceled;
theorem Th12: :: ZF_COLLA:12
theorem Th13: :: ZF_COLLA:13
theorem :: ZF_COLLA:14