[:(Day ((No_Ord A),A)),(Day ((No_Ord A),A)):] = ClosedProd ((No_Ord A),A,A) by Lm3;
hence No_Ord A is almost-No-order by Def12; :: thesis: verum