let FT be non empty RelStr ; :: thesis:
let A be Subset of FT; :: thesis:

hereby :: thesis:

assume A is open ; :: thesis:
then A1: A = A ^i by FIN_TOPO:def 16;
A2: for x being Element of FT st x in A holds
U_FT x c= A

let x be Element of FT; :: thesis:
assume x in A ; :: thesis:
then consider y being Element of FT such that
A3: ( x = y & U_FT y c= A ) by A1;
thus U_FT x c= A by A3; :: thesis:

end;

thus for z being Element of FT st U_FT z c= A holds
z in A by A1; :: thesis:
thus for x being Element of FT st x in A holds
U_FT x c= A by A2; :: thesis:

end;

assume A4: ( ( for z being Element of FT st U_FT z c= A holds
z in A ) & ( for x being Element of FT st x in A holds
U_FT x c= A ) ) ; :: thesis:
A5: A c= { y where y is Element of FT : U_FT y c= A }

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A6: u in A ; :: thesis:
then reconsider y2 = u as Element of FT ;
U_FT y2 c= A by A4, A6;
hence u in { y where y is Element of FT : U_FT y c= A } ; :: thesis:

end;

{ y where y is Element of FT : U_FT y c= A } c= A

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { y where y is Element of FT : U_FT y c= A } ; :: thesis:
then consider y being Element of FT such that
A7: ( y = u & U_FT y c= A ) ;
thus u in A by A4, A7; :: thesis:

end;

then A = A ^i by A5, XBOOLE_0:def 10;
hence A is open by FIN_TOPO:def 16; :: thesis: