{ (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } c= bool [: the carrier of T, the carrier of T:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } or x in bool [: the carrier of T, the carrier of T:] )
assume x in { (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } ; :: thesis: x in bool [: the carrier of T, the carrier of T:]
then ex O being Element of the topology of T st x = block_Pervin_quasi_uniformity O ;
hence x in bool [: the carrier of T, the carrier of T:] ; :: thesis: verum

end;

hence { (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } is Subset-Family of [: the carrier of T, the carrier of T:] ; :: thesis: verum