let L be TopSpace; :: thesis: 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 )
let G, ALL be set ; :: thesis: ( ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G ) } implies 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 ) )
assume A1: ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G ) } ; :: thesis: 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 )
set R = RelIncl ALL;
let M be set ; :: thesis: ( M is_minimal_in RelIncl ALL & M in field (RelIncl ALL) implies 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 ) )
assume that
A2: M is_minimal_in RelIncl ALL and
A3: M in field (RelIncl ALL) ; :: thesis: 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 )
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: ( A1 in M implies 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 ) )
assume A8: A1 in M ; :: thesis: 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 )
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: contradiction
A15: union C = [#] L by A6, SETFAM_1:45;
union (C \ {A1}) = the carrier of L

proof

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

per cases ( x in A1 or not x in A1 ) ;

suppose A17: x in A1 ; :: thesis: x in union (C \ {A1})

per cases ( x in A2 or x in A3 ) by A12, A17, XBOOLE_0:def 3;

suppose A18: x in A2 ; :: thesis: x in union (C \ {A1})

A2 in C \ {A1} by A5, A10, A13, ZFMISC_1:56;
hence x in union (C \ {A1}) by A18, TARSKI:def 4; :: thesis: verum

end;

suppose A19: x in A3 ; :: thesis: x in union (C \ {A1})

A3 in C \ {A1} by A5, A11, A14, ZFMISC_1:56;
hence x in union (C \ {A1}) by A19, TARSKI:def 4; :: thesis: verum

end;

end;

end;

suppose A20: not x in A1 ; :: thesis: x in union (C \ {A1})

consider Z being set such that
A21: x in Z and
A22: Z in C by A15, A16, TARSKI:def 4;
Z in C \ {A1} by A20, A21, A22, ZFMISC_1:56;
hence x in union (C \ {A1}) by A21, TARSKI:def 4; :: thesis: verum

end;

end;

end;

then A23: C \ {A1} is Cover of L by SETFAM_1:def 11;
A24: C \ {A1} c= M by A5, XBOOLE_1:36;
then C \ {A1} c= G by A5, A7;
then A25: C \ {A1} in ALL by A1, A23;
then [(C \ {A1}),M] in RelIncl ALL by A4, A3, A24, WELLORD2:def 1;
hence contradiction by A4, A2, A9, A25; :: thesis: verum