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 consider V1 being Subset of PT such that
A5: ( V1 = V & V1 is open & ex W being Subset of PT st
( W in FX & Cl V1 c= W ) ) by A4;
thus V is open by A5; :: 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 set ; :: 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
A6: ( x in V & V in FX ) by A2, PCOMPS_1:5;
reconsider V = V as Subset of PT ;

now

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

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

A8: x in (V ` ) ` by A6;
V is open by A3, A6, TOPS_2:def 1;
then V ` is closed by TOPS_1:30;
then consider X, Y being Subset of PT such that
A9: ( X is open & Y is open & x in X & V ` c= Y & X misses Y ) by A1, A7, A8, COMPTS_1:def 5;
A10: Y ` c= V by A9, SUBSET_1:36;
A11: X c= Y ` by A9, SUBSET_1:43;
Y ` is closed by A9, TOPS_1:30;
then Cl X c= Y ` by A11, TOPS_1:31;
then Cl X c= V by A10, XBOOLE_1:1;
then X in HX by A4, A6, A9;
hence x in union HX by A9, TARSKI:def 4; :: thesis: verum

end;

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

consider X being Subset of PT such that
A13: X = [#] PT ;
A14: V = ({} PT) ` by A12
.= [#] PT by PRE_TOPC:27 ;
A15: X is open by A13, TOPS_1:53;
A16: x in X by A13;
Cl X = V by A13, A14, TOPS_1:27;
then X in HX by A4, A6, A15;
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 12; :: 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