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;
( ( for x being Point of T holds Chi x,T c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T c= M ) holds
m c= M ) ) by Lm1;
hence Chi T = union { (Chi x,T) where x is Point of T : verum } by Def2; :: thesis: verum