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 :: thesis: for x being object holds
( x in P iff x in Int P )

let x be object ; :: 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 Th22; :: thesis: verum

end;

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