theorem Th47: :: RCOMP_3:47

for L being TopSpace
for G, G1 being Subset-Family of L st G is Cover of L & G is finite holds
for ALL being set st G1 = G \ { X where X is Subset of L : ( X in G & ex Y being Subset of L st
( Y in G & X c< Y ) ) } & ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } holds
ALL has_lower_Zorn_property_wrt RelIncl ALL