let A1, A2, B1, B2 be Ordinal; :: thesis: for R being Relation st ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) holds
OpenProd (R,A1,B1) c= OpenProd (R,A2,B2)
let R be Relation; :: thesis: ( ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) implies OpenProd (R,A1,B1) c= OpenProd (R,A2,B2) )
assume A1: ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) ; :: thesis: OpenProd (R,A1,B1) c= OpenProd (R,A2,B2)
A2: A1 c= A2 by A1, ORDINAL1:def 2;
A3: Day (R,A1) c= Day (R,A2) by A1, ORDINAL1:def 2, Th9;
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in OpenProd (R,A1,B1) or [x,y] in OpenProd (R,A2,B2) )
assume A4: [x,y] in OpenProd (R,A1,B1) ; :: thesis: [x,y] in OpenProd (R,A2,B2)
A5: ( x in Day (R,A1) & y in Day (R,A1) ) by A4, ZFMISC_1:87;
per cases ( ( born (R,x) in A1 & born (R,y) in A1 ) or ( born (R,x) = A1 & born (R,y) in B1 ) or ( born (R,x) in B1 & born (R,y) = A1 ) ) by A5, A4, Def9;
suppose ( born (R,x) in A1 & born (R,y) in A1 ) ; :: thesis: [x,y] in OpenProd (R,A2,B2)
hence [x,y] in OpenProd (R,A2,B2) by A2, A3, A5, Def9; :: thesis: verum
end;
suppose A6: ( born (R,x) = A1 & born (R,y) in B1 ) ; :: thesis: [x,y] in OpenProd (R,A2,B2)
per cases ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) by A1;
suppose A7: A1 in A2 ; :: thesis: [x,y] in OpenProd (R,A2,B2)
born (R,y) c= A1 by A5, Def8;
then born (R,y) in A2 by A7, ORDINAL1:12;
hence [x,y] in OpenProd (R,A2,B2) by A6, A7, A5, A3, Def9; :: thesis: verum
end;
suppose ( A1 = A2 & B1 c= B2 ) ; :: thesis: [x,y] in OpenProd (R,A2,B2)
hence [x,y] in OpenProd (R,A2,B2) by A6, A5, Def9; :: thesis: verum
end;
end;
end;
suppose A8: ( born (R,x) in B1 & born (R,y) = A1 ) ; :: thesis: [x,y] in OpenProd (R,A2,B2)
per cases ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) by A1;
suppose A9: A1 in A2 ; :: thesis: [x,y] in OpenProd (R,A2,B2)
born (R,x) c= A1 by A5, Def8;
then born (R,x) in A2 by A9, ORDINAL1:12;
hence [x,y] in OpenProd (R,A2,B2) by A8, A9, A5, A3, Def9; :: thesis: verum
end;
suppose ( A1 = A2 & B1 c= B2 ) ; :: thesis: [x,y] in OpenProd (R,A2,B2)
hence [x,y] in OpenProd (R,A2,B2) by A8, A5, Def9; :: thesis: verum
end;
end;
end;
end;