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 ) ) )

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 }

hence A is open ; :: thesis: verum

( 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 that 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

U_FT x c= A ; :: thesis: verum

end;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

hence
for x being Element of FT st x in A holds
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;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

U_FT x c= A ; :: thesis: verum

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

{ y where y is Element of FT : U_FT y c= A } c= A
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;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

proof

then
A = A ^i
by A4;
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;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

hence A is open ; :: thesis: verum