let b1, b2 be Ordinal; ( x in Day b1 & ( for O being Ordinal st x in Day O holds
b1 c= O ) & x in Day b2 & ( for O being Ordinal st x in Day O holds
b2 c= O ) implies b1 = b2 )
assume that
A8:
( x in Day b1 & ( for O being Ordinal st x in Day O holds
b1 c= O ) )
and
A9:
( x in Day b2 & ( for O being Ordinal st x in Day O holds
b2 c= O ) )
; b1 = b2
( b1 c= b2 & b2 c= b1 )
by A8, A9;
hence
b1 = b2
by XBOOLE_0:def 10; verum