let PT be non empty TopSpace; :: thesis: ( PT is regular implies for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) ) )
assume A1: PT is regular ; :: thesis: for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
let FX be Subset-Family of PT; :: thesis: ( FX is Cover of PT & FX is open implies ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) ) )
assume that
A2: FX is Cover of PT and
A3: FX is open ; :: thesis: ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
defpred S₁[ set ] means ex V1 being Subset of PT st
( V1 = $1 & V1 is open & ex W being Subset of PT st
( W in FX & Cl V1 c= W ) );
consider HX being Subset-Family of PT such that
A4: for V being Subset of PT holds
( V in HX iff S₁[V] ) from SUBSET_1:sch 3();
take HX ; :: thesis: ( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
for V being Subset of PT st V in HX holds
V is open

proof

let V be Subset of PT; :: thesis: ( V in HX implies V is open )
assume V in HX ; :: thesis: V is open
then ex V1 being Subset of PT st
( V1 = V & V1 is open & ex W being Subset of PT st
( W in FX & Cl V1 c= W ) ) by A4;
hence V is open ; :: thesis: verum

end;

hence HX is open by TOPS_2:def 1; :: thesis: ( HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
the carrier of PT c= union HX

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of PT or x in union HX )
assume x in the carrier of PT ; :: thesis: x in union HX
then reconsider x = x as Point of PT ;
consider V being Subset of PT such that
A5: x in V and
A6: V in FX by A2, PCOMPS_1:3;
reconsider V = V as Subset of PT ;

now :: thesis: x in union HX

per cases ( V ` <> {} or V ` = {} ) ;

suppose A7: V ` <> {} ; :: thesis: x in union HX

V is open by A3, A6, TOPS_2:def 1;
then A8: V ` is closed ;
x in (V `) ` by A5;
then consider X, Y being Subset of PT such that
A9: X is open and
A10: Y is open and
A11: x in X and
A12: V ` c= Y and
A13: X misses Y by A1, A7, A8, COMPTS_1:def 2;
( X c= Y ` & Y ` is closed ) by A10, A13, SUBSET_1:23;
then A14: Cl X c= Y ` by TOPS_1:5;
Y ` c= V by A12, SUBSET_1:17;
then Cl X c= V by A14;
then X in HX by A4, A6, A9;
hence x in union HX by A11, TARSKI:def 4; :: thesis: verum

end;

suppose A15: V ` = {} ; :: thesis: x in union HX

consider X being Subset of PT such that
A16: X = [#] PT ;
A17: X is open by A16;
V = ({} PT) ` by A15
.= [#] PT by PRE_TOPC:6 ;
then Cl X = V by A16, TOPS_1:2;
then X in HX by A4, A6, A17;
hence x in union HX by A16, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in union HX ; :: thesis: verum

end;

hence HX is Cover of PT by SETFAM_1:def 11; :: thesis: for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W )
let V be Subset of PT; :: thesis: ( V in HX implies ex W being Subset of PT st
( W in FX & Cl V c= W ) )
assume V in HX ; :: thesis: ex W being Subset of PT st
( W in FX & Cl V c= W )
then ex V1 being Subset of PT st
( V1 = V & V1 is open & ex W being Subset of PT st
( W in FX & Cl V1 c= W ) ) by A4;
hence ex W being Subset of PT st
( W in FX & Cl V c= W ) ; :: thesis: verum