let GX be TopSpace; :: thesis: for W being Subset-Family of GX st W is open & W is finite holds
meet W is open
let W be Subset-Family of GX; :: thesis: ( W is open & W is finite implies meet W is open )
assume that
A1: W is open and
A2: W is finite ; :: thesis: meet W is open
consider p being FinSequence such that
A3: rng p = W by A2, FINSEQ_1:52;
consider n being Nat such that
A4: dom p = Seg n by FINSEQ_1:def 2;
defpred S₁[ Nat] means for Z being Subset-Family of GX st Z = p .: (Seg $1) & $1 <= n & 1 <= n holds
meet Z is open ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: for Z being Subset-Family of GX st Z = p .: (Seg k) & k <= n & 1 <= n holds
meet Z is open ; :: thesis: S₁[k + 1]
let Z be Subset-Family of GX; :: thesis: ( Z = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies meet Z is open )
assume A7: Z = p .: (Seg (k + 1)) ; :: thesis: ( not k + 1 <= n or not 1 <= n or meet Z is open )
assume that
A8: k + 1 <= n and
A9: 1 <= n ; :: thesis: meet Z is open

A10: now :: thesis: ( 0 < k implies meet Z is open )

reconsider G2 = Im (p,(k + 1)) as Subset-Family of GX by A3, Th2, RELAT_1:111;
reconsider G1 = p .: (Seg k) as Subset-Family of GX by A3, Th2, RELAT_1:111;
assume A11: 0 < k ; :: thesis: meet Z is open
k + 1 <= n + 1 by A8, NAT_1:12;
then k <= n by XREAL_1:6;
then Seg k c= dom p by A4, FINSEQ_1:5;
then A12: G1 <> {} by A11, RELAT_1:119;
k + 1 <= n + 1 by A8, NAT_1:12;
then k <= n by XREAL_1:6;
then A13: meet G1 is open by A6, A9;
( 0 <= k & 0 + 1 = 1 ) by NAT_1:2;
then 1 <= k + 1 by XREAL_1:7;
then A14: k + 1 in dom p by A4, A8, FINSEQ_1:1;
then G2 = {(p . (k + 1))} by FUNCT_1:59;
then A15: meet G2 = p . (k + 1) by SETFAM_1:10;
{(k + 1)} c= dom p by A14, ZFMISC_1:31;
then A16: G2 <> {} by RELAT_1:119;
p . (k + 1) in W by A3, A14, FUNCT_1:def 3;
then A17: meet G2 is open by A1, A15;
p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ;
then meet Z = (meet G1) /\ (meet G2) by A7, A12, A16, SETFAM_1:9;
hence meet Z is open by A13, A17, TOPS_1:11; :: thesis: verum

end;

now :: thesis: ( k = 0 implies meet Z is open )

assume A18: k = 0 ; :: thesis: meet Z is open
then A19: 1 in dom p by A4, A8, FINSEQ_1:1;
then Im (p,1) = {(p . 1)} by FUNCT_1:59;
then meet Z = p . 1 by A7, A18, FINSEQ_1:2, SETFAM_1:10;
then meet Z in W by A3, A19, FUNCT_1:def 3;
hence meet Z is open by A1; :: thesis: verum

end;

hence meet Z is open by A10, NAT_1:3; :: thesis: verum

end;

A20: S₁[ 0 ]

proof

let Z be Subset-Family of GX; :: thesis: ( Z = p .: (Seg 0) & 0 <= n & 1 <= n implies meet Z is open )
assume that
A21: Z = p .: (Seg 0) and
0 <= n ; :: thesis: ( not 1 <= n or meet Z is open )
A22: {} in the topology of GX by PRE_TOPC:1;
meet Z = {} by A21, SETFAM_1:1;
hence ( not 1 <= n or meet Z is open ) by A22; :: thesis: verum

end;

A23: for k being Nat holds S₁[k] from NAT_1:sch 2(A20, A5);

A24: now :: thesis: ( 1 <= n implies meet W is open )

assume A25: 1 <= n ; :: thesis: meet W is open
W = p .: (Seg n) by A3, A4, RELAT_1:113;
hence meet W is open by A23, A25; :: thesis: verum

end;

A26: now :: thesis: ( n = 0 implies meet W is open )

assume n = 0 ; :: thesis: meet W is open
then Seg n = {} ;
then W = p .: {} by A3, A4, RELAT_1:113;
then A27: meet W = {} by SETFAM_1:1;
{} in the topology of GX by PRE_TOPC:1;
hence meet W is open by A27; :: thesis: verum

end;

now :: thesis: ( n <> 0 implies 1 <= n )

assume n <> 0 ; :: thesis: 1 <= n
then A28: 0 < n by NAT_1:3;
1 = 0 + 1 ;
hence 1 <= n by A28, NAT_1:13; :: thesis: verum

end;

hence meet W is open by A24, A26; :: thesis: verum