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