:: On Paracompactness of Metrizable Spaces
:: by Leszek Borys
::
:: Received July 23, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem :: PCOMPS_2:1
canceled;
theorem :: PCOMPS_2:2
canceled;
theorem :: PCOMPS_2:3
canceled;
theorem :: PCOMPS_2:4
canceled;
theorem Th5: :: PCOMPS_2:5
:: deftheorem defines PartUnion PCOMPS_2:def 1 :
:: deftheorem defines DisjointFam PCOMPS_2:def 2 :
:: deftheorem defines PartUnionNat PCOMPS_2:def 3 :
theorem Th6: :: PCOMPS_2:6
theorem :: PCOMPS_2:7
theorem Th8: :: PCOMPS_2:8
theorem :: PCOMPS_2:9
canceled;
theorem :: PCOMPS_2:10
canceled;
theorem :: PCOMPS_2:11
theorem Th12: :: PCOMPS_2:12
theorem :: PCOMPS_2:13