let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is closed holds
FinMeetCl F is closed
let F be Subset-Family of T; :: thesis: ( F is closed implies FinMeetCl F is closed )
assume A1: F is closed ; :: thesis: FinMeetCl F is closed

now

let P be Subset of T; :: thesis: ( P in FinMeetCl F implies P is closed )
assume P in FinMeetCl F ; :: thesis: P is closed
then consider Y being Subset-Family of T such that
A2: ( Y c= F & Y is finite & P = Intersect Y ) by CANTOR_1:def 4;
A3: for A being Subset of T st A in Y holds
A is closed by A1, A2, TOPS_2:def 2;
( ( P = the carrier of T & the carrier of T = [#] T ) or P = meet Y ) by A2, SETFAM_1:def 10;
hence P is closed by A3, PRE_TOPC:44; :: thesis: verum

end;

hence FinMeetCl F is closed by TOPS_2:def 2; :: thesis: verum