let TS be TopSpace; :: thesis: for x being set
for K being Subset of TS holds
( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )
let x be set ; :: thesis: for K being Subset of TS holds
( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )
let K be Subset of TS; :: thesis: ( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )
thus ( x in Int K implies ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) ) by Th16; :: thesis: ( ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) implies x in Int K )
given Q being Subset of TS such that A1: Q is open and
A2: Q c= K and
A3: x in Q ; :: thesis: x in Int K
K ` c= Q ` by A2, SUBSET_1:12;
then Cl (K `) c= Cl (Q `) by PRE_TOPC:19;
then Cl (K `) c= Q ` by A1, PRE_TOPC:22;
then (Q `) ` c= (Cl (K `)) ` by SUBSET_1:12;
hence x in Int K by A3; :: thesis: verum