consider R being Relation such that
A1: ( R preserves_No_Comparison_on ClosedProd (R,A,A) & R c= ClosedProd (R,A,A) ) by Th28;
take R ; :: thesis: ( R preserves_No_Comparison_on [:(Day (R,A)),(Day (R,A)):] & R c= [:(Day (R,A)),(Day (R,A)):] )
thus ( R preserves_No_Comparison_on [:(Day (R,A)),(Day (R,A)):] & R c= [:(Day (R,A)),(Day (R,A)):] ) by A1, Lm3; :: thesis: verum