theorem Th4: :: TOPGEN_2:4

for T being non empty TopStruct holds Chi T = union { (Chi (x,T)) where x is Point of T : verum }