for L being TopSpace
for G, ALL being set st ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G ) } holds
for M being set st M is_minimal_in RelIncl ALL & M in field (RelIncl ALL) holds
for A1 being Subset of L st A1 in M holds
for A2, A3 being Subset of L holds
( not A2 in M or not A3 in M or not A1 c= A2 \/ A3 or not A1 <> A2 or not A1 <> A3 )