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 )

( 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

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

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;now :: thesis: for W being object st W in A -extension_of_the_topology_of X holds

W in the topology of X

then A6:
A -extension_of_the_topology_of X c= the topology of X
by TARSKI:def 3;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;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

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