let it1, it2 be Ordinal; :: thesis: ( o in Day (R,it1) & ( for O being Ordinal st o in Day (R,O) holds
it1 c= O ) & o in Day (R,it2) & ( for O being Ordinal st o in Day (R,O) holds
it2 c= O ) implies it1 = it2 )
assume that
A3: ( o in Day (R,it1) & ( for O being Ordinal st o in Day (R,O) holds
it1 c= O ) ) and
A4: ( o in Day (R,it2) & ( for O being Ordinal st o in Day (R,O) holds
it2 c= O ) ) ; :: thesis: it1 = it2
( it1 c= it2 & it2 c= it1 ) by A3, A4;
hence it1 = it2 by XBOOLE_0:def 10; :: thesis: verum