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

suppose A2: F <> {} ; :: thesis:

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 )

let x be set ; :: thesis:
assume A5: x in the carrier of GX ; :: thesis:
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:

assume A6: for A being Subset of GX st A in F holds
x in A ; :: thesis:
let Z be Subset of GX; :: thesis:
assume Z in R1 ; :: thesis:
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:

end;

assume A7: for Z being Subset of GX st Z in R1 holds
not x in Z ; :: thesis:
let A be Subset of GX; :: thesis:
assume A8: A in F ; :: thesis:
([#] 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:

end;

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

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

assume A10: x in ([#] GX) \ (union R1) ; :: thesis:
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:

end;

assume A11: x in meet F ; :: thesis:
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:

end;

let B be object ; :: thesis:
assume A12: B in R1 ; :: thesis:
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:

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:

end;

suppose A15: F = {} ; :: thesis:

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:

end;

end;