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 ex E being open Subset of X st
( E = P & [:([#] Y),E:] c= union (Base-Appr ([#] [:Y,X:])) ) by A1;
hence P is open ; :: 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 k9 = k as Point of X ;
reconsider Z = [:([#] Y),{k9}:] as Subset of [:Y,X:] ;
Z c= [#] [:Y,X:] ;
then Z c= union (Base-Appr ([#] [:Y,X:])) by BORSUK_1:13;
then A3: Base-Appr ([#] [:Y,X:]) is Cover of Z by SETFAM_1:def 11;
Z is compact by Th18;
then consider G being Subset-Family of [:Y,X:] such that
A4: G c= Base-Appr ([#] [:Y,X:]) and
A5: G is Cover of Z and
G is finite by A3, COMPTS_1:def 4;
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 ex x1 being Point of X st
( k = x1 & [:([#] Y),{x1}:] c= union G ) ;
hence k in the carrier of X ; :: thesis: verum

end;

then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } as Subset of X ;
Z c= union G by A5, SETFAM_1:def 11;
then A6: k9 in Q ;
A7: [:([#] 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
A8: x1 in [#] Y and
A9: x2 in Q and
A10: z = [x1,x2] by ZFMISC_1:def 2;
consider x29 being Point of X such that
A11: x29 = x2 and
A12: [:([#] Y),{x29}:] c= union G by A9;
x2 in {x29} by A11, TARSKI:def 1;
then A13: z in [:([#] Y),{x29}:] by A8, A10, ZFMISC_1:87;
union G c= union (Base-Appr ([#] [:Y,X:])) by A4, ZFMISC_1:77;
then [:([#] Y),{x29}:] c= union (Base-Appr ([#] [:Y,X:])) by A12, XBOOLE_1:1;
hence z in union (Base-Appr ([#] [:Y,X:])) by A13; :: thesis: verum

end;

union G is open by A4, TOPS_2:11, TOPS_2:19;
then Q in the topology of X by Th14;
then Q is open by PRE_TOPC:def 2;
then Q in R by A1, A7;
hence k in union R by A6, TARSKI:def 4; :: thesis: verum

end;

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