let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is open iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A )
let A be Subset of X; :: thesis: ( A is open iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A )
thus ( A is open implies TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A ) :: thesis: ( TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A implies A is open )

proof

assume A is open ; :: thesis: TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A
then A in the topology of X by PRE_TOPC:def 2;
hence TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A by Th92; :: thesis: verum

end;

thus ( TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A implies A is open ) :: thesis: verum

proof

assume TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A ; :: thesis: A is open
then A in the topology of X by Th92;
hence A is open by PRE_TOPC:def 2; :: thesis: verum

end;