defpred S₁[ object , object ] means ( ( born (R,$1) in A & born (R,$2) in A ) or ( born (R,$1) = A & born (R,$2) in B ) or ( born (R,$1) in B & born (R,$2) = A ) );
let I1, I2 be Relation of (Day (R,A)); :: thesis: ( ( for x, y being Element of Day (R,A) holds
( [x,y] in I1 iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) ) ) & ( for x, y being Element of Day (R,A) holds
( [x,y] in I2 iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) ) ) implies I1 = I2 )
assume that
A1: for x, y being Element of Day (R,A) holds
( [x,y] in I1 iff S₁[x,y] ) and
A2: for x, y being Element of Day (R,A) holds
( [x,y] in I2 iff S₁[x,y] ) ; :: thesis: I1 = I2
I1 = I2 from RELSET_1:sch 4(A1, A2);
hence I1 = I2 ; :: thesis: verum