let A be Ordinal; :: thesis: for a, b being object holds
( [a,b] in ClosedProd ((No_Ord A),A,A) iff ( a in Day A & b in Day A ) )
let a, b be object ; :: thesis: ( [a,b] in ClosedProd ((No_Ord A),A,A) iff ( a in Day A & b in Day A ) )
thus ( [a,b] in ClosedProd ((No_Ord A),A,A) implies ( a in Day A & b in Day A ) ) by ZFMISC_1:87; :: thesis: ( a in Day A & b in Day A implies [a,b] in ClosedProd ((No_Ord A),A,A) )
assume A1: ( a in Day A & b in Day A ) ; :: thesis: [a,b] in ClosedProd ((No_Ord A),A,A)
then ( born ((No_Ord A),a) c= A & born ((No_Ord A),b) c= A ) by Def8;
then ( ( born ((No_Ord A),a) in A & born ((No_Ord A),b) in A ) or ( born ((No_Ord A),a) = A & born ((No_Ord A),b) c= A ) or ( born ((No_Ord A),a) c= A & born ((No_Ord A),b) = A ) or ( born ((No_Ord A),a) = A & born ((No_Ord A),b) = A ) ) by ORDINAL1:11, XBOOLE_0:def 8;
hence [a,b] in ClosedProd ((No_Ord A),A,A) by Def10, A1; :: thesis: verum