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