let FT be non empty RelStr ; :: thesis: for A being Subset of FT holds
( A is open iff ( ( 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 ) ) )
let A be Subset of FT; :: thesis: ( A is open iff ( ( 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 ) ) )

hereby :: thesis: ( ( 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 ) implies A is open )

assume A is open ; :: thesis: ( ( 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 ) )
then A1: A = A ^i ;
hence for z being Element of FT st U_FT z c= A holds
z in A ; :: thesis: for x being Element of FT st x in A holds
U_FT x c= A
for x being Element of FT st x in A holds
U_FT x c= A

proof

let x be Element of FT; :: thesis: ( x in A implies U_FT x c= A )
assume x in A ; :: thesis: U_FT x c= A
then ex y being Element of FT st
( x = y & U_FT y c= A ) by A1;
hence U_FT x c= A ; :: thesis: verum

end;

hence for x being Element of FT st x in A holds
U_FT x c= A ; :: thesis: verum

end;

assume that
A2: for z being Element of FT st U_FT z c= A holds
z in A and
A3: for x being Element of FT st x in A holds
U_FT x c= A ; :: thesis: A is open
A4: A c= { y where y is Element of FT : U_FT y c= A }

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in A or u in { y where y is Element of FT : U_FT y c= A } )
assume A5: u in A ; :: thesis: u in { y where y is Element of FT : U_FT y c= A }
then reconsider y2 = u as Element of FT ;
U_FT y2 c= A by A3, A5;
hence u in { y where y is Element of FT : U_FT y c= A } ; :: thesis: verum

end;

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

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { y where y is Element of FT : U_FT y c= A } or u in A )
assume u in { y where y is Element of FT : U_FT y c= A } ; :: thesis: u in A
then ex y being Element of FT st
( y = u & U_FT y c= A ) ;
hence u in A by A2; :: thesis: verum

end;

then A = A ^i by A4;
hence A is open ; :: thesis: verum