take M0 = MetrStruct(# 1,Empty^2-to-zero #); :: thesis: ( M0 is strict & M0 is ultra & M0 is Reflexive & M0 is symmetric & M0 is Discerning & M0 is triangle )
M0 is ultra by Th24;
hence ( M0 is strict & M0 is ultra & M0 is Reflexive & M0 is symmetric & M0 is Discerning & M0 is triangle ) ; :: thesis: verum