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 :: thesis: for W being object st W in A -extension_of_the_topology_of X holds
W in the topology of X
let W be object ; :: 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 ;
A5: G /\ A is open by A1, A4, PRE_TOPC:def 1;
H1 is open by A3;
then H1 \/ (G /\ A) is open by A5;
hence W in the topology of X by A2; :: 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 Th88;
hence the topology of X = A -extension_of_the_topology_of X by A6; :: thesis: verum
end;
thus ( the topology of X = A -extension_of_the_topology_of X implies A in the topology of X ) by Th91; :: thesis: verum