let X, Y be non empty compact TopSpace; :: thesis: for R being Subset-Family of X st R = { Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:])) } holds
( R is open & R is Cover of [#] X )
let R be Subset-Family of X; :: thesis: ( R = { Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:])) } implies ( R is open & R is Cover of [#] X ) )
assume A1: R = { Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:])) } ; :: thesis: ( R is open & R is Cover of [#] X )

now

let P be Subset of X; :: thesis: ( P in R implies P is open )
assume P in R ; :: thesis: P is open
then consider E being open Subset of X such that
A2: ( E = P & [:([#] Y),E:] c= union (Base-Appr ([#] [:Y,X:])) ) by A1;
thus P is open by A2; :: thesis: verum

end;

hence R is open by TOPS_2:def 1; :: thesis: R is Cover of [#] X
[#] X c= union R

proof

let k be set ; :: according to TARSKI:def 3 :: thesis: ( not k in [#] X or k in union R )
assume k in [#] X ; :: thesis: k in union R
then reconsider k' = k as Point of X ;
reconsider Z = [:([#] Y),{k'}:] as Subset of [:Y,X:] ;
Z c= [#] [:Y,X:] ;
then Z c= union (Base-Appr ([#] [:Y,X:])) by BORSUK_1:54;
then A3: Base-Appr ([#] [:Y,X:]) is Cover of Z by SETFAM_1:def 12;
A4: Base-Appr ([#] [:Y,X:]) is open by BORSUK_1:51;
Z is compact by Th18;
then consider G being Subset-Family of [:Y,X:] such that
A5: ( G c= Base-Appr ([#] [:Y,X:]) & G is Cover of Z & G is finite ) by A3, A4, COMPTS_1:def 7;
A6: Z c= union G by A5, SETFAM_1:def 12;
set uR = union G;
set Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } ;
{ x where x is Point of X : [:([#] Y),{x}:] c= union G } c= the carrier of X

proof

let k be set ; :: according to TARSKI:def 3 :: thesis: ( not k in { x where x is Point of X : [:([#] Y),{x}:] c= union G } or k in the carrier of X )
assume k in { x where x is Point of X : [:([#] Y),{x}:] c= union G } ; :: thesis: k in the carrier of X
then consider x1 being Point of X such that
A7: ( k = x1 & [:([#] Y),{x1}:] c= union G ) ;
thus k in the carrier of X by A7; :: thesis: verum

end;

then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } as Subset of X ;
union G is open by A4, A5, TOPS_2:18, TOPS_2:26;
then Q in the topology of X by Th14;
then A8: Q is open by PRE_TOPC:def 5;
A9: k' in Q by A6;
[:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:]))

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:([#] Y),Q:] or z in union (Base-Appr ([#] [:Y,X:])) )
assume z in [:([#] Y),Q:] ; :: thesis: z in union (Base-Appr ([#] [:Y,X:]))
then consider x1, x2 being set such that
A10: ( x1 in [#] Y & x2 in Q & z = [x1,x2] ) by ZFMISC_1:def 2;
consider x2' being Point of X such that
A11: ( x2' = x2 & [:([#] Y),{x2'}:] c= union G ) by A10;
union G c= union (Base-Appr ([#] [:Y,X:])) by A5, ZFMISC_1:95;
then A12: [:([#] Y),{x2'}:] c= union (Base-Appr ([#] [:Y,X:])) by A11, XBOOLE_1:1;
x2 in {x2'} by A11, TARSKI:def 1;
then z in [:([#] Y),{x2'}:] by A10, ZFMISC_1:106;
hence z in union (Base-Appr ([#] [:Y,X:])) by A12; :: thesis: verum

end;

then Q in R by A1, A8;
hence k in union R by A9, TARSKI:def 4; :: thesis: verum

end;

hence R is Cover of [#] X by SETFAM_1:def 12; :: thesis: verum