theorem Th45: :: RCOMP_3:45

for T being 1-sorted
for F being finite Subset-Family of T
for F1 being Subset-Family of T st F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } holds
F1 is Cover of T