let X be non empty set ; :: thesis: for D being a_partition of X holds OpenClosedSet (partition_topology D) = the topology of (partition_topology D)
let D be a_partition of X; :: thesis: OpenClosedSet (partition_topology D) = the topology of (partition_topology D)
thus OpenClosedSet (partition_topology D) c= the topology of (partition_topology D) :: according to XBOOLE_0:def 10 :: thesis: the topology of (partition_topology D) c= OpenClosedSet (partition_topology D)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenClosedSet (partition_topology D) or x in the topology of (partition_topology D) )
assume x in OpenClosedSet (partition_topology D) ; :: thesis: x in the topology of (partition_topology D)
then ex y being Subset of (partition_topology D) st
( x = y & y is open & y is closed ) ;
hence x in the topology of (partition_topology D) ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (partition_topology D) or x in OpenClosedSet (partition_topology D) )
assume A2: x in the topology of (partition_topology D) ; :: thesis: x in OpenClosedSet (partition_topology D)
then reconsider y = x as Subset of (partition_topology D) ;
y is open by A2;
then ( y is open & y is closed ) by Th18;
hence x in OpenClosedSet (partition_topology D) ; :: thesis: verum