0. (TOP-REAL 3) = 0* 3 by EUCLID:70
.= 3 |-> 0 by EUCLID:def 4
.= <*0,0,0*> by FINSEQ_2:62 ;
hence 0. (TOP-REAL 3) = |[0,0,0]| ; :: thesis: verum