let L be 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 )
let G, ALL be set ; ( 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 ) }
; 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 ; ( 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)
; 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; ( 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
; 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
; contradiction
A15:
union C = [#] L
by A6, SETFAM_1:45;
union (C \ {A1}) = the carrier of L
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; verum