let GX be TopSpace; :: thesis: for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is closed ) holds
meet F is closed
let F be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX st A in F holds
A is closed ) implies meet F is closed )
assume A1: for A being Subset of GX st A in F holds
A is closed ; :: thesis: meet F is closed

per cases ( F <> {} or F = {} ) ;

suppose A2: F <> {} ; :: thesis: meet F is closed

defpred S₁[ set ] means ([#] GX) \ $1 in F;
consider R1 being Subset-Family of GX such that
A3: for B being Subset of GX holds
( B in R1 iff S₁[B] ) from SUBSET_1:sch 3();

now

let B be set ; :: thesis: ( B in R1 implies B in the topology of GX )
assume A4: B in R1 ; :: thesis: B in the topology of GX
then reconsider B1 = B as Subset of GX ;
A5: ([#] GX) \ (([#] GX) \ B1) = B1 by Th22;
( B1 in R1 iff ([#] GX) \ B1 in F ) by A3;
then ([#] GX) \ B1 is closed by A1, A4;
then B1 is open by A5, Def6;
hence B in the topology of GX by Def5; :: thesis: verum

end;

then R1 c= the topology of GX by TARSKI:def 3;
then union R1 in the topology of GX by Def1;
then A6: union R1 is open by Def5;
([#] GX) \ (([#] GX) \ (union R1)) = union R1 by Th22;
then A7: ([#] GX) \ (union R1) is closed by A6, Def6;
A8: for x being set st x in the carrier of GX holds
( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z )

proof

let x be set ; :: thesis: ( x in the carrier of GX implies ( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z ) )
assume A9: x in the carrier of GX ; :: thesis: ( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z )
thus ( ( for A being Subset of GX st A in F holds
x in A ) implies for Z being Subset of GX st Z in R1 holds
not x in Z ) :: thesis: ( ( for Z being Subset of GX st Z in R1 holds
not x in Z ) implies for A being Subset of GX st A in F holds
x in A )

proof

assume A10: for A being Subset of GX st A in F holds
x in A ; :: thesis: for Z being Subset of GX st Z in R1 holds
not x in Z
let Z be Subset of GX; :: thesis: ( Z in R1 implies not x in Z )
assume Z in R1 ; :: thesis: not x in Z
then ([#] GX) \ Z in F by A3;
then x in ([#] GX) \ Z by A10;
hence not x in Z by XBOOLE_0:def 5; :: thesis: verum

end;

assume A11: for Z being Subset of GX st Z in R1 holds
not x in Z ; :: thesis: for A being Subset of GX st A in F holds
x in A
let A be Subset of GX; :: thesis: ( A in F implies x in A )
assume A12: A in F ; :: thesis: x in A
([#] GX) \ (([#] GX) \ A) = A by Th22;
then ([#] GX) \ A in R1 by A3, A12;
then not x in ([#] GX) \ A by A11;
hence x in A by A9, XBOOLE_0:def 5; :: thesis: verum

end;

for x being set holds
( x in ([#] GX) \ (union R1) iff x in meet F )

proof

let x be set ; :: thesis: ( x in ([#] GX) \ (union R1) iff x in meet F )
thus ( x in ([#] GX) \ (union R1) implies x in meet F ) :: thesis: ( x in meet F implies x in ([#] GX) \ (union R1) )

proof

assume A13: x in ([#] GX) \ (union R1) ; :: thesis: x in meet F
then not x in union R1 by XBOOLE_0:def 5;
then for Z being Subset of GX st Z in R1 holds
not x in Z by TARSKI:def 4;
then for A being set st A in F holds
x in A by A8, A13;
hence x in meet F by A2, SETFAM_1:def 1; :: thesis: verum

end;

assume A14: x in meet F ; :: thesis: x in ([#] GX) \ (union R1)
then for A being Subset of GX st A in F holds
x in A by SETFAM_1:def 1;
then for Z being set st x in Z holds
not Z in R1 by A8;
then not x in union R1 by TARSKI:def 4;
hence x in ([#] GX) \ (union R1) by A14, XBOOLE_0:def 5; :: thesis: verum

end;

hence meet F is closed by A7, TARSKI:2; :: thesis: verum

end;

suppose A15: F = {} ; :: thesis: meet F is closed

{} GX is closed

proof

the carrier of GX in the topology of GX by Def1;
then A16: [#] GX is open by Def5;
[#] GX = ([#] GX) \ ({} GX) ;
hence {} GX is closed by A16, Def6; :: thesis: verum

end;

hence meet F is closed by A15, SETFAM_1:def 1; :: thesis: verum

end;

end;