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