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
A2: dom f = NAT and
A3: 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
A4: for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A1);
A5: 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 A4; :: thesis: verum

end;

now

thus dom f = NAT by A2; :: 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 x in NAT ; :: thesis: f . b₁ in bool [:(Fin the carrier of R),(Fin the carrier of R):]
then reconsider x9 = x as Element of NAT ;

per cases ( x9 = 0 or x9 > 0 ) ;

suppose A6: x9 = 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 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):]
then ex a, b being Element of Fin the carrier of R st
( z = [a,b] & ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) ) ;
hence z in [:(Fin the carrier of R),(Fin the carrier of R):] ; :: 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 A3, A6; :: thesis: verum

end;

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

A8: x9 = (x9 - 1) + 1 ;
reconsider x1 = x9 - 1 as Element of NAT by A7, 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 ) } ;
A9: { [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 . x9 by A4, A8;

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 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):]
then ex a, b being Element of Fin the carrier of R st
( z = [a,b] & a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in f . x1 ) ;
hence z in [:(Fin the carrier of R),(Fin the carrier of R):] ; :: 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 A9; :: 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 A2, A3, A5; :: thesis: verum