let A, B be RelStr ; :: thesis: MonFuncs (A,B) c= Funcs ( the carrier of A, the carrier of B)

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in MonFuncs (A,B) or a in Funcs ( the carrier of A, the carrier of B) )

assume a in MonFuncs (A,B) ; :: thesis: a in Funcs ( the carrier of A, the carrier of B)

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 Def6;

hence a in Funcs ( the carrier of A, the carrier of B) ; :: thesis: verum

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in MonFuncs (A,B) or a in Funcs ( the carrier of A, the carrier of B) )

assume a in MonFuncs (A,B) ; :: thesis: a in Funcs ( the carrier of A, the carrier of B)

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 Def6;

hence a in Funcs ( the carrier of A, the carrier of B) ; :: thesis: verum