let A, B be RelStr ; :: thesis: MonFuncs A,B c= Funcs the carrier of A,the carrier of B
let a be set ; :: 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 consider f being Function of A,B such that
A1: ( a = f & f in Funcs the carrier of A,the carrier of B & f is monotone ) by Def6;
thus a in Funcs the carrier of A,the carrier of B by A1; :: thesis: verum