let A1, A2 be set ; :: thesis: ( ( for a being set holds
( a in A1 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) & ( for a being set holds
( a in A2 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) implies A1 = A2 )
assume that
A5: for a being set holds
( a in A1 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) and
A6: for a being set holds
( a in A2 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ; :: thesis: A1 = A2
for a being object st a in A2 holds
a in A1

proof

let a be object ; :: thesis: ( a in A2 implies a in A1 )
assume a in A2 ; :: thesis: a in A1
then ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A6;
hence a in A1 by A5; :: thesis: verum

end;

then A7: A2 c= A1 ;
for a being object st a in A1 holds
a in A2

proof

let a be object ; :: thesis: ( a in A1 implies a in A2 )
assume a in A1 ; :: thesis: a in A2
then ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A5;
hence a in A2 by A6; :: thesis: verum

end;

then A1 c= A2 ;
hence A1 = A2 by A7; :: thesis: verum