let T be non empty TopStruct ; :: thesis: for x being Point of T holds Chi (x,T) c= Chi T
set X = { (Chi (x,T)) where x is Point of T : verum } ;
let x be Point of T; :: thesis: Chi (x,T) c= Chi T
A1: Chi (x,T) in { (Chi (x,T)) where x is Point of T : verum } ;
Chi T = union { (Chi (x,T)) where x is Point of T : verum } by Th4;
hence Chi (x,T) c= Chi T by A1, ZFMISC_1:74; :: thesis: verum