let L be TopSpace; :: thesis:
let G, ALL be set ; :: thesis:
assume A1: ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G ) } ; :: thesis:
set R = RelIncl ALL;
let M be set ; :: thesis:
assume that
A2: M is_minimal_in RelIncl ALL and
A3: M in field (RelIncl ALL) ; :: thesis:
A4: field (RelIncl ALL) = ALL by WELLORD2:def 1;
then consider C being Subset-Family of L such that
A5: M = C and
A6: C is Cover of L and
A7: C c= G by A1, A3;
let A1 be Subset of L; :: thesis:
assume A8: A1 in M ; :: thesis:
set Y = C \ {A1};
A9: C \ {A1} <> M by A8, ZFMISC_1:56;
given A2, A3 being Subset of L such that A10: A2 in M and
A11: A3 in M and
A12: A1 c= A2 \/ A3 and
A13: A1 <> A2 and
A14: A1 <> A3 ; :: thesis:
A15: union C = [#] L by A6, SETFAM_1:45;
union (C \ {A1}) = the carrier of L

thus union (C \ {A1}) c= the carrier of L ; :: according to XBOOLE_0:def 10 :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A16: x in the carrier of L ; :: thesis:

end;

end;

end;