let S1, S2 be RelStr ; :: thesis: for D being Subset of S1
for f being Function of S1,S2 st f is monotone holds
f .: () c= downarrow (f .: D)

let D be Subset of S1; :: thesis: for f being Function of S1,S2 st f is monotone holds
f .: () c= downarrow (f .: D)

let f be Function of S1,S2; :: thesis: ( f is monotone implies f .: () c= downarrow (f .: D) )
assume A1: f is monotone ; :: thesis: f .: () c= downarrow (f .: D)
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in f .: () or q in downarrow (f .: D) )
assume A2: q in f .: () ; :: thesis: q in downarrow (f .: D)
then consider x being object such that
A3: x in dom f and
A4: x in downarrow D and
A5: q = f . x by FUNCT_1:def 6;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A2;
reconsider x = x as Element of s1 by A3;
consider y being Element of s1 such that
A6: x <= y and
A7: y in D by ;
reconsider f1 = f as Function of s1,s2 ;
f1 . x is Element of s2 ;
then reconsider q1 = q, fy = f1 . y as Element of s2 by A5;
the carrier of s2 <> {} ;
then dom f = the carrier of s1 by FUNCT_2:def 1;
then A8: f . y in f .: D by ;
q1 <= fy by A1, A5, A6;
hence q in downarrow (f .: D) by ; :: thesis: verum