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 :: thesis: for P being Subset of X st P in R holds
P is open

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 ; :: thesis: R is Cover of [#] X
[#] X c= union R

proof

let k be object ; :: 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 A2: Base-Appr ([#] [:Y,X:]) is Cover of Z by SETFAM_1:def 11;
Z is compact by Th16;
then consider G being Subset-Family of [:Y,X:] such that
A3: G c= Base-Appr ([#] [:Y,X:]) and
A4: G is Cover of Z and
G is finite by A2;
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 object ; :: 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 A4, SETFAM_1:def 11;
then A5: k9 in Q ;
A6: [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:]))

proof

let z be object ; :: 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 object such that
A7: x1 in [#] Y and
A8: x2 in Q and
A9: z = [x1,x2] by ZFMISC_1:def 2;
consider x29 being Point of X such that
A10: x29 = x2 and
A11: [:([#] Y),{x29}:] c= union G by A8;
x2 in {x29} by A10, TARSKI:def 1;
then A12: z in [:([#] Y),{x29}:] by A7, A9, ZFMISC_1:87;
union G c= union (Base-Appr ([#] [:Y,X:])) by A3, ZFMISC_1:77;
then [:([#] Y),{x29}:] c= union (Base-Appr ([#] [:Y,X:])) by A11;
hence z in union (Base-Appr ([#] [:Y,X:])) by A12; :: thesis: verum

end;

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

end;

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