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
A2: A -extension_of_the_topology_of X c= the topology of X

proof

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
A3: W = H \/ (G /\ A) and
A4: ( H in the topology of X & 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 ( H1 is open & G /\ A is open ) by A4, PRE_TOPC:def 5;
then H1 \/ (G /\ A) is open by TOPS_1:37;
hence W in the topology of X by A3, PRE_TOPC:def 5; :: thesis: verum

end;

hence A -extension_of_the_topology_of X c= the topology of X by TARSKI:def 3; :: thesis: verum

end;

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 A2, 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