let S1, S2 be RelStr ; 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; 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; ( f is monotone implies f .: (downarrow D) c= downarrow (f .: D) )
assume A1:
f is monotone
; f .: (downarrow D) c= downarrow (f .: D)
let q be object ; TARSKI:def 3 ( not q in f .: (downarrow D) or q in downarrow (f .: D) )
assume A2:
q in f .: (downarrow D)
; 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; verum