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 set ; :: 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 set such that
A3: ( x in dom f & x in downarrow D & q = f . x ) by FUNCT_1:def 12;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A2, A3;
reconsider f1 = f as Function of s1,s2 ;
reconsider x = x as Element of s1 by A3;
consider y being Element of s1 such that
A4: ( x <= y & y in D ) by A3, WAYBEL_0:def 15;
f1 . x is Element of s2 ;
then reconsider q1 = q, fy = f1 . y as Element of s2 by A3;
A5: q1 <= fy by A1, A3, A4, ORDERS_3:def 5;
the carrier of s2 <> {} ;
then dom f = the carrier of s1 by FUNCT_2:def 1;
then f . y in f .: D by A4, FUNCT_1:def 12;
hence q in downarrow (f .: D) by A5, WAYBEL_0:def 15; :: thesis: verum