let A, B be RelStr ; MonFuncs (A,B) c= Funcs ( the carrier of A, the carrier of B)
let a be object ; TARSKI:def 3 ( not a in MonFuncs (A,B) or a in Funcs ( the carrier of A, the carrier of B) )
assume
a in MonFuncs (A,B)
; 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)
; verum