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