let T be non empty TopStruct ; :: thesis: Chi T = union { (Chi x,T) where x is Point of T : verum }
set X = { (Chi x,T) where x is Point of T : verum } ;
reconsider m = union { (Chi x,T) where x is Point of T : verum } as cardinal number by Lm1;
A1: for M being cardinal number st ( for x being Point of T holds Chi x,T c= M ) holds
m c= M by Lm1;
for x being Point of T holds Chi x,T c= m by Lm1;
hence Chi T = union { (Chi x,T) where x is Point of T : verum } by A1, Def2; :: thesis: verum