let L1, L2 be non empty RelStr ; :: thesis: for g being Function of L1,L2 holds inclusion g is monotone
let g be Function of L1,L2; :: thesis: inclusion g is monotone
let s1, s2 be Element of (Image g); :: according to WAYBEL_1:def 2 :: thesis: ( s1 <= s2 implies (inclusion g) . s1 <= (inclusion g) . s2 )
assume s1 <= s2 ; :: thesis: (inclusion g) . s1 <= (inclusion g) . s2
then (id (Image g)) . s1 <= s2 by FUNCT_1:35;
then (id (Image g)) . s1 <= (id (Image g)) . s2 by FUNCT_1:35;
hence (inclusion g) . s1 <= (inclusion g) . s2 by YELLOW_0:60; :: thesis: verum