let T be TopSpace; :: thesis:
let F be Subset-Family of T; :: thesis:
assume A1: F is finite ; :: thesis:
A2: meet (Int F) c= Int (meet F)

proof

consider p being FinSequence such that
A3: rng p = F by A1, FINSEQ_1:52;
consider n being Nat such that
A4: dom p = Seg n by FINSEQ_1:def 2;
defpred S₁[ Nat] means for G being Subset-Family of T st G = p .: (Seg $1) & $1 <= n & 1 <= n holds
meet (Int G) c= Int (meet G);
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A6: for G being Subset-Family of T st G = p .: (Seg k) & k <= n & 1 <= n holds
meet (Int G) c= Int (meet G) ; :: thesis:
let G be Subset-Family of T; :: thesis:
assume A7: G = p .: (Seg (k + 1)) ; :: thesis:
assume that
A8: k + 1 <= n and
A9: 1 <= n ; :: thesis:

A10: now :: thesis:

reconsider G2 = Im (p,(k + 1)) as Subset-Family of T by A3, RELAT_1:111, TOPS_2:2;
reconsider G1 = p .: (Seg k) as Subset-Family of T by A3, RELAT_1:111, TOPS_2:2;
A11: 0 + 1 = 1 ;
0 <= k by NAT_1:2;
then 1 <= k + 1 by A11, XREAL_1:7;
then A12: k + 1 in dom p by A4, A8, FINSEQ_1:1;
then A13: G2 = {(p . (k + 1))} by FUNCT_1:59;
then meet G2 = p . (k + 1) by SETFAM_1:10;
then reconsider G3 = p . (k + 1) as Subset of T ;
A14: meet (Int G2) = meet {(Int G3)} by A13, Th19
.= Int G3 by SETFAM_1:10
.= Int (meet G2) by A13, SETFAM_1:10 ;
k + 1 <= n + 1 by A8, NAT_1:12;
then k <= n by XREAL_1:6;
then A15: meet (Int G1) c= Int (meet G1) by A6, A9;
assume 0 < k ; :: thesis:
then A16: 0 + 1 <= k by NAT_1:13;
then A17: k in Seg k by FINSEQ_1:1;
k <= n by A8, NAT_1:13;
then k in dom p by A4, A16, FINSEQ_1:1;
then A18: p . k in G1 by A17, FUNCT_1:def 6;
k + 1 in {(k + 1)} by TARSKI:def 1;
then A19: p . (k + 1) in G2 by A12, FUNCT_1:def 6;
then A20: Int G2 <> {} by Th18;
A21: p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ;
then Int (meet G) = Int ((meet G1) /\ (meet G2)) by A7, A18, A19, SETFAM_1:9
.= (Int (meet G1)) /\ (Int (meet G2)) by TOPS_1:17 ;
then A22: (meet (Int G1)) /\ (meet (Int G2)) c= Int (meet G) by A14, A15, XBOOLE_1:27;
Int G1 <> {} by A18, Th18;
then meet ((Int G1) \/ (Int G2)) c= Int (meet G) by A20, A22, SETFAM_1:9;
hence meet (Int G) c= Int (meet G) by A7, A21, Th21; :: thesis:

end;

now :: thesis:

assume A23: k = 0 ; :: thesis:
then 1 in dom p by A4, A8, FINSEQ_1:1;
then A24: Im (p,1) = {(p . 1)} by FUNCT_1:59;
then union G = p . 1 by A7, A23, FINSEQ_1:2, ZFMISC_1:25;
then reconsider G1 = p . 1 as Subset of T ;
Int (meet G) = Int G1 by A7, A23, A24, FINSEQ_1:2, SETFAM_1:10
.= meet {(Int G1)} by SETFAM_1:10
.= meet (Int G) by A7, A23, A24, Th19, FINSEQ_1:2 ;
hence meet (Int G) c= Int (meet G) ; :: thesis:

end;

hence meet (Int G) c= Int (meet G) by A10, NAT_1:3; :: thesis:

end;

A25: S₁[ 0 ] by Th18, SETFAM_1:1;
A26: for k being Nat holds S₁[k] from NAT_1:sch 2(A25, A5);

A27: now :: thesis:

assume A28: 1 <= n ; :: thesis:
F = p .: (Seg n) by A3, A4, RELAT_1:113;
hence meet (Int F) c= Int (meet F) by A26, A28; :: thesis:

end;

A29: now :: thesis:

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

end;

now :: thesis:

assume n = 0 ; :: thesis:
then Seg n = {} ;
then F = p .: {} by A3, A4, RELAT_1:113;
then F = {} ;
hence meet (Int F) c= Int (meet F) by Th18, SETFAM_1:1; :: thesis:

end;

hence meet (Int F) c= Int (meet F) by A27, A29; :: thesis:

end;

Int (meet F) c= meet (Int F) by Th28;
hence Int (meet F) = meet (Int F) by A2, XBOOLE_0:def 10; :: thesis: