let TS be TopSpace; :: thesis: for P being Subset of TS holds
( P is open iff for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) )
let P be Subset of TS; :: thesis: ( P is open iff for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) )
thus ( P is open implies for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) ) ; :: thesis: ( ( for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) ) implies P is open )
assume A1: for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) ; :: thesis: P is open

now

let x be set ; :: thesis: ( x in P iff x in Int P )
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) by A1;
hence ( x in P iff x in Int P ) by Th54; :: thesis: verum

end;

hence P is open by TARSKI:1; :: thesis: verum