set IR = the InternalRel of R;
set CR = the carrier of R;
set FBCP = [:(Fin the carrier of R),(Fin the carrier of R):];
let IT1, IT2 be sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]); ( dom IT1 = NAT & IT1 . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds IT1 . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in IT1 . n ) } ) & dom IT2 = NAT & IT2 . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds IT2 . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in IT2 . n ) } ) implies IT1 = IT2 )
assume that
A10:
dom IT1 = NAT
and
A11:
IT1 . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) }
and
A12:
for n being Nat holds IT1 . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in IT1 . n ) }
and
A13:
dom IT2 = NAT
and
A14:
IT2 . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) }
and
A15:
for n being Nat holds IT2 . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in IT2 . n ) }
; IT1 = IT2
defpred S1[ Nat, set , set ] means $3 = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in $2 ) } ;
A16:
dom IT1 = NAT
by A10;
A17:
IT1 . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) }
by A11;
A18:
for n being Nat holds S1[n,IT1 . n,IT1 . (n + 1)]
by A12;
A19:
dom IT2 = NAT
by A13;
A20:
IT2 . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) }
by A14;
A21:
for n being Nat holds S1[n,IT2 . n,IT2 . (n + 1)]
by A15;
A22:
for n being Nat
for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
;
thus
IT1 = IT2
from NAT_1:sch 13(A16, A17, A18, A19, A20, A21, A22); verum