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();
A4: 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 A5: 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 A6: 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 A6;
hence not x in Z by XBOOLE_0:def 5; :: thesis: verum

end;

assume A7: 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 A8: A in F ; :: thesis: x in A
([#] GX) \ (([#] GX) \ A) = A by Th3;
then ([#] GX) \ A in R1 by A3, A8;
then not x in ([#] GX) \ A by A7;
hence x in A by A5, XBOOLE_0:def 5; :: thesis: verum

end;

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

proof

let x be object ; :: 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 A10: 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 A4, A10;
hence x in meet F by A2, SETFAM_1:def 1; :: thesis: verum

end;

assume A11: 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 A4;
then not x in union R1 by TARSKI:def 4;
hence x in ([#] GX) \ (union R1) by A11, XBOOLE_0:def 5; :: thesis: verum

end;

now :: thesis: for B being object st B in R1 holds
B in the topology of GX

let B be object ; :: thesis: ( B in R1 implies B in the topology of GX )
assume A12: B in R1 ; :: thesis: B in the topology of GX
then reconsider B1 = B as Subset of GX ;
( B1 in R1 iff ([#] GX) \ B1 in F ) by A3;
then A13: ([#] GX) \ B1 is closed by A1, A12;
([#] GX) \ (([#] GX) \ B1) = B1 by Th3;
then B1 is open by A13;
hence B in the topology of GX ; :: thesis: verum

end;

then R1 c= the topology of GX ;
then union R1 in the topology of GX by Def1;
then A14: union R1 is open ;
([#] GX) \ (([#] GX) \ (union R1)) = union R1 by Th3;
then ([#] GX) \ (union R1) is closed by A14;
hence meet F is closed by A9, TARSKI:2; :: thesis: verum

end;

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

the carrier of GX in the topology of GX by Def1;
then A16: [#] GX is open ;
{} GX is closed by A16;
hence meet F is closed by A15, SETFAM_1:def 1; :: thesis: verum

end;

end;