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

for a being object st a in A1 holds

a in A2

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

( 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

then A7:
A2 c= A1
;
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;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

for a being object st a in A1 holds

a in A2

proof

then
A1 c= A2
;
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;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

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