let L1, L2 be non empty RelStr ; :: thesis: for f being Function of L1,L2
for X being Subset of L1
for x being Element of L1 st f is monotone & x is_<=_than X holds
f . x is_<=_than f .: X
let g be Function of L1,L2; :: thesis: for X being Subset of L1
for x being Element of L1 st g is monotone & x is_<=_than X holds
g . x is_<=_than g .: X
let X be Subset of L1; :: thesis: for x being Element of L1 st g is monotone & x is_<=_than X holds
g . x is_<=_than g .: X
let x be Element of L1; :: thesis: ( g is monotone & x is_<=_than X implies g . x is_<=_than g .: X )
assume that
A1: g is monotone and
A2: x is_<=_than X ; :: thesis: g . x is_<=_than g .: X
let y2 be Element of L2; :: according to LATTICE3:def 8 :: thesis: ( not y2 in g .: X or g . x <= y2 )
assume y2 in g .: X ; :: thesis: g . x <= y2
then consider x2 being Element of L1 such that
A3: x2 in X and
A4: y2 = g . x2 by FUNCT_2:65;
reconsider x2 = x2 as Element of L1 ;
x <= x2 by A2, A3;
hence g . x <= y2 by A1, A4; :: thesis: verum