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

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 :: thesis: for P being Subset of T st P in FinMeetCl F holds

P is closed

hence
FinMeetCl F is closed
; :: thesis: verumP is closed

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 and

Y is finite and

A3: P = Intersect Y by CANTOR_1:def 3;

A4: ( ( P = the carrier of T & the carrier of T = [#] T ) or P = meet Y ) by A3, SETFAM_1:def 9;

for A being Subset of T st A in Y holds

A is closed by A1, A2;

hence P is closed by A4, PRE_TOPC:14; :: thesis: verum

end;assume P in FinMeetCl F ; :: thesis: P is closed

then consider Y being Subset-Family of T such that

A2: Y c= F and

Y is finite and

A3: P = Intersect Y by CANTOR_1:def 3;

A4: ( ( P = the carrier of T & the carrier of T = [#] T ) or P = meet Y ) by A3, SETFAM_1:def 9;

for A being Subset of T st A in Y holds

A is closed by A1, A2;

hence P is closed by A4, PRE_TOPC:14; :: thesis: verum