{} c= A ;
then Day (R,{}) c= Day (R,A) by Th9;
hence not Day (R,A) is empty by Th8; :: thesis: verum