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:92; :: thesis: verum