let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A in the topology of X iff the topology of X = A -extension_of_the_topology_of X )
let A be Subset of X; :: thesis: ( A in the topology of X iff the topology of X = A -extension_of_the_topology_of X )
thus ( A in the topology of X implies the topology of X = A -extension_of_the_topology_of X ) :: thesis: ( the topology of X = A -extension_of_the_topology_of X implies A in the topology of X )

proof

assume A1: A in the topology of X ; :: thesis: the topology of X = A -extension_of_the_topology_of X

now

let W be set ; :: thesis: ( W in A -extension_of_the_topology_of X implies W in the topology of X )
assume W in A -extension_of_the_topology_of X ; :: thesis: W in the topology of X
then consider H, G being Subset of X such that
A2: W = H \/ (G /\ A) and
A3: H in the topology of X and
A4: G in the topology of X ;
reconsider H1 = H as Subset of X ;
G /\ A in the topology of X by A1, A4, PRE_TOPC:def 1;
then A5: G /\ A is open by PRE_TOPC:def 2;
H1 is open by A3, PRE_TOPC:def 2;
then H1 \/ (G /\ A) is open by A5;
hence W in the topology of X by A2, PRE_TOPC:def 2; :: thesis: verum

end;

then A6: A -extension_of_the_topology_of X c= the topology of X by TARSKI:def 3;
the topology of X c= A -extension_of_the_topology_of X by Th99;
hence the topology of X = A -extension_of_the_topology_of X by A6, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( the topology of X = A -extension_of_the_topology_of X implies A in the topology of X ) by Th102; :: thesis: verum