:: The Reflection Theorem
:: by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: ZF_REFLE:1
canceled;
theorem Th2: :: ZF_REFLE:2
theorem Th3: :: ZF_REFLE:3
theorem Th4: :: ZF_REFLE:4
theorem Th5: :: ZF_REFLE:5
theorem Th6: :: ZF_REFLE:6
theorem :: ZF_REFLE:7
theorem Th8: :: ZF_REFLE:8
:: deftheorem defines union ZF_REFLE:def 1 :
theorem :: ZF_REFLE:9
canceled;
theorem Th10: :: ZF_REFLE:10
theorem Th11: :: ZF_REFLE:11
theorem :: ZF_REFLE:12
theorem Th13: :: ZF_REFLE:13
theorem Th14: :: ZF_REFLE:14
theorem Th15: :: ZF_REFLE:15
theorem :: ZF_REFLE:16
canceled;
theorem Th17: :: ZF_REFLE:17
:: deftheorem ZF_REFLE:def 2 :
canceled;
:: deftheorem ZF_REFLE:def 3 :
canceled;
:: deftheorem ZF_REFLE:def 4 :
canceled;
:: deftheorem Def5 defines DOMAIN-yielding ZF_REFLE:def 5 :
theorem :: ZF_REFLE:18
canceled;
theorem :: ZF_REFLE:19
canceled;
theorem :: ZF_REFLE:20
canceled;
theorem :: ZF_REFLE:21
canceled;
theorem :: ZF_REFLE:22
canceled;
theorem Th23: :: ZF_REFLE:23
theorem Th24: :: ZF_REFLE:24
theorem Th25: :: ZF_REFLE:25
theorem :: ZF_REFLE:26
canceled;
theorem :: ZF_REFLE:27
theorem Th28: :: ZF_REFLE:28
theorem :: ZF_REFLE:29