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 .: (downarrow D) c= downarrow (f .: D)

let D be Subset of S1; :: thesis: for f being Function of S1,S2 st f is monotone holds

f .: (downarrow D) c= downarrow (f .: D)

let f be Function of S1,S2; :: thesis: ( f is monotone implies f .: (downarrow D) c= downarrow (f .: D) )

assume A1: f is monotone ; :: thesis: f .: (downarrow D) c= downarrow (f .: D)

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in f .: (downarrow D) or q in downarrow (f .: D) )

assume A2: q in f .: (downarrow D) ; :: 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 A4, WAYBEL_0:def 15;

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 A7, FUNCT_1:def 6;

q1 <= fy by A1, A5, A6;

hence q in downarrow (f .: D) by A8, WAYBEL_0:def 15; :: thesis: verum

for f being Function of S1,S2 st f is monotone holds

f .: (downarrow D) c= downarrow (f .: D)

let D be Subset of S1; :: thesis: for f being Function of S1,S2 st f is monotone holds

f .: (downarrow D) c= downarrow (f .: D)

let f be Function of S1,S2; :: thesis: ( f is monotone implies f .: (downarrow D) c= downarrow (f .: D) )

assume A1: f is monotone ; :: thesis: f .: (downarrow D) c= downarrow (f .: D)

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in f .: (downarrow D) or q in downarrow (f .: D) )

assume A2: q in f .: (downarrow D) ; :: 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 A4, WAYBEL_0:def 15;

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 A7, FUNCT_1:def 6;

q1 <= fy by A1, A5, A6;

hence q in downarrow (f .: D) by A8, WAYBEL_0:def 15; :: thesis: verum