{ (block_Pervin_uniformity A) where A is Element of SF : verum } c= bool [:X,X:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (block_Pervin_uniformity A) where A is Element of SF : verum } or x in bool [:X,X:] )
assume x in { (block_Pervin_uniformity A) where A is Element of SF : verum } ; :: thesis: x in bool [:X,X:]
then consider A being Element of SF such that
A1: x = block_Pervin_uniformity A ;
thus x in bool [:X,X:] by A1; :: thesis: verum

end;

hence { (block_Pervin_uniformity A) where A is Element of SF : verum } is Subset-Family of [:X,X:] ; :: thesis: verum