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 .: (uparrow D) c= uparrow (f .: D)
let D be Subset of S1; :: thesis: for f being Function of S1,S2 st f is monotone holds
f .: (uparrow D) c= uparrow (f .: D)
let f be Function of S1,S2; :: thesis: ( f is monotone implies f .: (uparrow D) c= uparrow (f .: D) )
assume A1: f is monotone ; :: thesis: f .: (uparrow D) c= uparrow (f .: D)
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in f .: (uparrow D) or q in uparrow (f .: D) )
assume A2: q in f .: (uparrow D) ; :: thesis: q in uparrow (f .: D)
then consider x being object such that
A3: x in dom f and
A4: x in uparrow 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: y <= x and
A7: y in D by A4, WAYBEL_0:def 16;
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;
fy <= q1 by A1, A5, A6;
hence q in uparrow (f .: D) by A8, WAYBEL_0:def 16; :: thesis: verum