set IR = the InternalRel of R;
set CR = the carrier of R;
set FBCP = [:(Fin the carrier of R),(Fin the carrier of R):];
defpred S₁[ 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 ) } ;
A1: for n being Element of NAT
for x being set ex y being set st S₁[n,x,y] ;
consider f being Function such that
A3: dom f = NAT and
A4: f . 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
A5: for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A1);
B5: for n being Nat holds S₁[n,f . n,f . (n + 1)]

proof

let n be Nat; :: thesis: S₁[n,f . n,f . (n + 1)]
n in NAT by ORDINAL1:def 13;
hence S₁[n,f . n,f . (n + 1)] by A5; :: thesis: verum

end;

now

thus dom f = NAT by A3; :: thesis: for x being set st x in NAT holds
f . b₂ in bool [:(Fin the carrier of R),(Fin the carrier of R):]
let x be set ; :: thesis: ( x in NAT implies f . b₁ in bool [:(Fin the carrier of R),(Fin the carrier of R):] )
assume A6: x in NAT ; :: thesis: f . b₁ in bool [:(Fin the carrier of R),(Fin the carrier of R):]
reconsider x' = x as Element of NAT by A6;

per cases ( x' = 0 or x' > 0 ) ;

suppose A7: x' = 0 ; :: thesis: f . b₁ in bool [:(Fin the carrier of R),(Fin the carrier of R):]

set F0 = { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } ;

now

let z be set ; :: thesis: ( z in { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } implies z in [:(Fin the carrier of R),(Fin the carrier of R):] )
assume A8: z in { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } ; :: thesis: z in [:(Fin the carrier of R),(Fin the carrier of R):]
consider a, b being Element of Fin the carrier of R such that
A9: z = [a,b] and
( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) by A8;
thus z in [:(Fin the carrier of R),(Fin the carrier of R):] by A9; :: thesis: verum

end;

then { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } c= [:(Fin the carrier of R),(Fin the carrier of R):] by TARSKI:def 3;
hence f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] by A4, A7; :: thesis: verum

end;

suppose A10: x' > 0 ; :: thesis: f . b₁ in bool [:(Fin the carrier of R),(Fin the carrier of R):]

A11: x' = (x' - 1) + 1 ;
reconsider x1 = x' - 1 as Element of NAT by A10, NAT_1:20;
set FX = { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } ;
A12: { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } = f . x by A5, A11;

now

let z be set ; :: thesis: ( z in { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } implies z in [:(Fin the carrier of R),(Fin the carrier of R):] )
assume A13: z in { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } ; :: thesis: z in [:(Fin the carrier of R),(Fin the carrier of R):]
consider a, b being Element of Fin the carrier of R such that
A14: ( z = [a,b] & a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) by A13;
thus z in [:(Fin the carrier of R),(Fin the carrier of R):] by A14; :: thesis: verum

end;

then { [a,b] where a, b is Element of Fin the carrier of R : ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) } c= [:(Fin the carrier of R),(Fin the carrier of R):] by TARSKI:def 3;
hence f . x in bool [:(Fin the carrier of R),(Fin the carrier of R):] by A12; :: thesis: verum

end;

end;

end;

then reconsider f = f as Function of NAT ,(bool [:(Fin the carrier of R),(Fin the carrier of R):]) by FUNCT_2:5;
take f ; :: thesis: ( dom f = NAT & f . 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 f . (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 f . n ) } ) )
thus ( dom f = NAT & f . 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 f . (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 f . n ) } ) ) by A3, A4, B5; :: thesis: verum