let L1, L2 be non empty RelStr ; :: thesis: for g being Function of L1,L2 st g is monotone holds
corestr g is monotone
let g be Function of L1,L2; :: thesis: ( g is monotone implies corestr g is monotone )
assume A1: g is monotone ; :: thesis: corestr g is monotone
let s1, s2 be Element of L1; :: according to WAYBEL_1:def 2 :: thesis: ( s1 <= s2 implies (corestr g) . s1 <= (corestr g) . s2 )
assume s1 <= s2 ; :: thesis: (corestr g) . s1 <= (corestr g) . s2
then A2: g . s1 <= g . s2 by A1;
reconsider s19 = g . s1, s29 = g . s2 as Element of L2 ;
( s19 = (corestr g) . s1 & s29 = (corestr g) . s2 ) by Th30;
hence (corestr g) . s1 <= (corestr g) . s2 by A2, YELLOW_0:60; :: thesis: verum