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 )
reconsider s1' = g . s1, s2' = g . s2 as Element of L2 ;
A2: ( s1' = (corestr g) . s1 & s2' = (corestr g) . s2 ) by Th32;
assume s1 <= s2 ; :: thesis: (corestr g) . s1 <= (corestr g) . s2
then g . s1 <= g . s2 by A1, Def2;
hence (corestr g) . s1 <= (corestr g) . s2 by A2, YELLOW_0:61; :: thesis: verum