set N = { i where i is Element of NAT : ( m < i & f . i = b ) } ;
consider j being Element of NAT such that
A2: ( m < j & f . j = b ) by A1;
A3: j in { i where i is Element of NAT : ( m < i & f . i = b ) } by A2;

now

let x be set ; :: thesis: ( x in { i where i is Element of NAT : ( m < i & f . i = b ) } implies x in NAT )
assume x in { i where i is Element of NAT : ( m < i & f . i = b ) } ; :: thesis: x in NAT
then consider i being Element of NAT such that
A4: x = i and
( m < i & f . i = b ) ;
thus x in NAT by A4; :: thesis: verum

end;

then reconsider N = { i where i is Element of NAT : ( m < i & f . i = b ) } as non empty Subset of NAT by A3, TARSKI:def 3;
take I = min N; :: thesis: ( f . I = b & m < I & ( for i being Element of NAT st m < i & f . i = b holds
I <= i ) )
I in N by XXREAL_2:def 7;
then consider II being Element of NAT such that
A5: ( II = I & m < II & f . II = b ) ;
thus ( f . I = b & m < I ) by A5; :: thesis: for i being Element of NAT st m < i & f . i = b holds
I <= i
let i be Element of NAT ; :: thesis: ( m < i & f . i = b implies I <= i )
assume A6: ( m < i & f . i = b ) ; :: thesis: I <= i
i in N by A6;
hence I <= i by XXREAL_2:def 7; :: thesis: verum