let X, Y be non empty TopSpace; :: thesis: for t being Point of Y

for A being Subset of X st A is compact holds

for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

let t be Point of Y; :: thesis: for A being Subset of X st A is compact holds

for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

let A be Subset of X; :: thesis: ( A is compact implies for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G )

assume A1: A is compact ; :: thesis: for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

let G be a_neighborhood of [:A,{t}:]; :: thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;

for A being Subset of X st A is compact holds

for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

let t be Point of Y; :: thesis: for A being Subset of X st A is compact holds

for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

let A be Subset of X; :: thesis: ( A is compact implies for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G )

assume A1: A is compact ; :: thesis: for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

let G be a_neighborhood of [:A,{t}:]; :: thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;

now :: thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= Gend;

hence
ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
; :: thesis: verumper cases
( A <> {} X or A = {} X )
;

end;

suppose A3:
A <> {} X
; :: thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

[:A,{t}:] c= Int G
by CONNSP_2:def 2;

then [:A,{t}:] c= union (Base-Appr G) by Th14;

then Base-Appr G is Cover of [:A,{t}:] by SETFAM_1:def 11;

then consider K being Subset-Family of [:X,Y:] such that

A4: K c= Base-Appr G and

A5: K is Cover of [:A,{t}:] and

A6: for c being set st c in K holds

c meets [:A,{t}:] by Th22;

reconsider PK = (Pr1 (X,Y)) .: K as Subset-Family of X ;

K is open by A4, TOPS_2:11;

then A7: (Pr1 (X,Y)) .: K is open by Th19;

PK is Cover of A by A5, Th21;

then consider M being Subset-Family of X such that

A8: M c= (Pr1 (X,Y)) .: K and

A9: M is Cover of A and

A10: M is finite by A1, A7, COMPTS_1:def 4;

consider N being Subset-Family of [:X,Y:] such that

A11: N c= K and

A12: N is finite and

A13: (Pr1 (X,Y)) .: N = M by A8, A10, Th23;

reconsider F = (Pr1 (X,Y)) .: N as Subset-Family of X ;

A14: N is Cover of [:A,{t}:]

then A26: A c= union F by SETFAM_1:def 11;

reconsider H = (Pr2 (X,Y)) .: N as Subset-Family of Y ;

then N <> {} by A3, ZFMISC_1:2;

then H <> {} by Th20;

then A34: t in meet H by A27, SETFAM_1:def 1;

A35: N c= Base-Appr G by A4, A11;

then A36: N is open by TOPS_2:11;

then meet H is open by A12, Th19, TOPS_2:20;

then t in Int (meet H) by A34, TOPS_1:23;

then reconsider W = meet H as a_neighborhood of t by CONNSP_2:def 1;

union F is open by A36, Th19, TOPS_2:19;

then A c= Int (union F) by A26, TOPS_1:23;

then reconsider V = union F as a_neighborhood of A by CONNSP_2:def 2;

take V = V; :: thesis: ex W being a_neighborhood of t st [:V,W:] c= G

take W = W; :: thesis: [:V,W:] c= G

end;then [:A,{t}:] c= union (Base-Appr G) by Th14;

then Base-Appr G is Cover of [:A,{t}:] by SETFAM_1:def 11;

then consider K being Subset-Family of [:X,Y:] such that

A4: K c= Base-Appr G and

A5: K is Cover of [:A,{t}:] and

A6: for c being set st c in K holds

c meets [:A,{t}:] by Th22;

reconsider PK = (Pr1 (X,Y)) .: K as Subset-Family of X ;

K is open by A4, TOPS_2:11;

then A7: (Pr1 (X,Y)) .: K is open by Th19;

PK is Cover of A by A5, Th21;

then consider M being Subset-Family of X such that

A8: M c= (Pr1 (X,Y)) .: K and

A9: M is Cover of A and

A10: M is finite by A1, A7, COMPTS_1:def 4;

consider N being Subset-Family of [:X,Y:] such that

A11: N c= K and

A12: N is finite and

A13: (Pr1 (X,Y)) .: N = M by A8, A10, Th23;

reconsider F = (Pr1 (X,Y)) .: N as Subset-Family of X ;

A14: N is Cover of [:A,{t}:]

proof

then
F is Cover of A
by Th21;
let e1, e2 be object ; :: according to RELAT_1:def 3,SETFAM_1:def 11 :: thesis: ( not [e1,e2] in [:A,{t}:] or [e1,e2] in union N )

A15: A c= union M by A9, SETFAM_1:def 11;

assume A16: [e1,e2] in [:A,{t}:] ; :: thesis: [e1,e2] in union N

then [e1,e2] `2 in {t} by MCART_1:10;

then [e1,e2] `2 = t by TARSKI:def 1;

then A17: [e1,e2] = [([e1,e2] `1),t] ;

[e1,e2] `1 in A by A16, MCART_1:10;

then consider X1 being set such that

A18: [e1,e2] `1 in X1 and

A19: X1 in M by A15, TARSKI:def 4;

consider XY being Subset of [:X,Y:] such that

A20: XY in N and

A21: (Pr1 (X,Y)) . XY = X1 by A13, A19, FUNCT_2:65;

XY in K by A11, A20;

then XY in Base-Appr G by A4;

then consider X2 being Subset of X, Y2 being Subset of Y such that

A22: XY = [:X2,Y2:] and

[:X2,Y2:] c= G and

X2 is open and

Y2 is open ;

XY meets [:A,{t}:] by A6, A11, A20;

then consider xy being object such that

A23: xy in XY and

A24: xy in [:A,{t}:] by XBOOLE_0:3;

xy `2 in {t} by A24, MCART_1:10;

then xy `2 = t by TARSKI:def 1;

then A25: t in Y2 by A22, A23, MCART_1:10;

XY <> {} by A18, A21, FUNCT_3:8;

then [e1,e2] `1 in X2 by A18, A21, A22, EQREL_1:50;

then [e1,e2] in [:X2,Y2:] by A25, A17, ZFMISC_1:87;

hence [e1,e2] in union N by A20, A22, TARSKI:def 4; :: thesis: verum

end;A15: A c= union M by A9, SETFAM_1:def 11;

assume A16: [e1,e2] in [:A,{t}:] ; :: thesis: [e1,e2] in union N

then [e1,e2] `2 in {t} by MCART_1:10;

then [e1,e2] `2 = t by TARSKI:def 1;

then A17: [e1,e2] = [([e1,e2] `1),t] ;

[e1,e2] `1 in A by A16, MCART_1:10;

then consider X1 being set such that

A18: [e1,e2] `1 in X1 and

A19: X1 in M by A15, TARSKI:def 4;

consider XY being Subset of [:X,Y:] such that

A20: XY in N and

A21: (Pr1 (X,Y)) . XY = X1 by A13, A19, FUNCT_2:65;

XY in K by A11, A20;

then XY in Base-Appr G by A4;

then consider X2 being Subset of X, Y2 being Subset of Y such that

A22: XY = [:X2,Y2:] and

[:X2,Y2:] c= G and

X2 is open and

Y2 is open ;

XY meets [:A,{t}:] by A6, A11, A20;

then consider xy being object such that

A23: xy in XY and

A24: xy in [:A,{t}:] by XBOOLE_0:3;

xy `2 in {t} by A24, MCART_1:10;

then xy `2 = t by TARSKI:def 1;

then A25: t in Y2 by A22, A23, MCART_1:10;

XY <> {} by A18, A21, FUNCT_3:8;

then [e1,e2] `1 in X2 by A18, A21, A22, EQREL_1:50;

then [e1,e2] in [:X2,Y2:] by A25, A17, ZFMISC_1:87;

hence [e1,e2] in union N by A20, A22, TARSKI:def 4; :: thesis: verum

then A26: A c= union F by SETFAM_1:def 11;

reconsider H = (Pr2 (X,Y)) .: N as Subset-Family of Y ;

A27: now :: thesis: for C being set st C in H holds

t in C

[:A,{t}:] c= union N
by A14, SETFAM_1:def 11;t in C

let C be set ; :: thesis: ( C in H implies t in C )

assume C in H ; :: thesis: t in C

then consider D being Subset of [:X,Y:] such that

A28: D in N and

A29: C = (pr2 ( the carrier of X, the carrier of Y)) .: D by Th17;

D meets [:A,{t}:] by A6, A11, A28;

then D /\ [:A,{t}:] <> {} ;

then consider x being Point of [:X,Y:] such that

A30: x in D /\ [:A,{t}:] ;

A31: x in [:A,{t}:] by A30, XBOOLE_0:def 4;

then x `1 in A by MCART_1:10;

then A32: (pr2 ( the carrier of X, the carrier of Y)) . ((x `1),t) = t by FUNCT_3:def 5;

x `2 in {t} by A31, MCART_1:10;

then x `2 = t by TARSKI:def 1;

then A33: x = [(x `1),t] by A2, MCART_1:21;

x in D by A30, XBOOLE_0:def 4;

hence t in C by A2, A29, A33, A32, FUNCT_2:35; :: thesis: verum

end;assume C in H ; :: thesis: t in C

then consider D being Subset of [:X,Y:] such that

A28: D in N and

A29: C = (pr2 ( the carrier of X, the carrier of Y)) .: D by Th17;

D meets [:A,{t}:] by A6, A11, A28;

then D /\ [:A,{t}:] <> {} ;

then consider x being Point of [:X,Y:] such that

A30: x in D /\ [:A,{t}:] ;

A31: x in [:A,{t}:] by A30, XBOOLE_0:def 4;

then x `1 in A by MCART_1:10;

then A32: (pr2 ( the carrier of X, the carrier of Y)) . ((x `1),t) = t by FUNCT_3:def 5;

x `2 in {t} by A31, MCART_1:10;

then x `2 = t by TARSKI:def 1;

then A33: x = [(x `1),t] by A2, MCART_1:21;

x in D by A30, XBOOLE_0:def 4;

hence t in C by A2, A29, A33, A32, FUNCT_2:35; :: thesis: verum

then N <> {} by A3, ZFMISC_1:2;

then H <> {} by Th20;

then A34: t in meet H by A27, SETFAM_1:def 1;

A35: N c= Base-Appr G by A4, A11;

then A36: N is open by TOPS_2:11;

then meet H is open by A12, Th19, TOPS_2:20;

then t in Int (meet H) by A34, TOPS_1:23;

then reconsider W = meet H as a_neighborhood of t by CONNSP_2:def 1;

union F is open by A36, Th19, TOPS_2:19;

then A c= Int (union F) by A26, TOPS_1:23;

then reconsider V = union F as a_neighborhood of A by CONNSP_2:def 2;

take V = V; :: thesis: ex W being a_neighborhood of t st [:V,W:] c= G

take W = W; :: thesis: [:V,W:] c= G

now :: thesis: for e being set st e in N holds

( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] )

hence
[:V,W:] c= G
by Th15; :: thesis: verum( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] )

let e be set ; :: thesis: ( e in N implies ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) )

assume e in N ; :: thesis: ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] )

then e in Base-Appr G by A35;

then ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open ) ;

hence ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; :: thesis: verum

end;assume e in N ; :: thesis: ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] )

then e in Base-Appr G by A35;

then ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open ) ;

hence ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; :: thesis: verum

suppose
A = {} X
; :: thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

then
A c= Int ({} X)
;

then reconsider V = {} X as a_neighborhood of A by CONNSP_2:def 2;

set W = the a_neighborhood of t;

take V = V; :: thesis: ex W being a_neighborhood of t st [:V,W:] c= G

take W = the a_neighborhood of t; :: thesis: [:V,W:] c= G

thus [:V,W:] c= G ; :: thesis: verum

end;then reconsider V = {} X as a_neighborhood of A by CONNSP_2:def 2;

set W = the a_neighborhood of t;

take V = V; :: thesis: ex W being a_neighborhood of t st [:V,W:] c= G

take W = the a_neighborhood of t; :: thesis: [:V,W:] c= G

thus [:V,W:] c= G ; :: thesis: verum