let S be reflexive RelStr ; :: thesis: for T being reflexive transitive RelStr
for f being Function of S,T
for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))
let T be reflexive transitive RelStr ; :: thesis: for f being Function of S,T
for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))
let f be Function of S,T; :: thesis: for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))
let X be Subset of S; :: thesis: ( f is monotone implies downarrow (f .: X) = downarrow (f .: (downarrow X)) )
assume A1: f is monotone ; :: thesis: downarrow (f .: X) = downarrow (f .: (downarrow X))
thus downarrow (f .: X) c= downarrow (f .: (downarrow X)) by Th6; :: according to XBOOLE_0:def 10 :: thesis: downarrow (f .: (downarrow X)) c= downarrow (f .: X)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in downarrow (f .: (downarrow X)) or a in downarrow (f .: X) )
assume A2: a in downarrow (f .: (downarrow X)) ; :: thesis: a in downarrow (f .: X)
then reconsider T1 = T as non empty reflexive transitive RelStr ;
reconsider b = a as Element of T1 by A2;
consider fx being Element of T1 such that
A3: fx >= b and
A4: fx in f .: (downarrow X) by A2, WAYBEL_0:def 15;
consider x being object such that
A5: x in dom f and
A6: x in downarrow X and
A7: fx = f . x by A4, FUNCT_1:def 6;
reconsider S1 = S as non empty reflexive RelStr by A5;
reconsider x = x as Element of S1 by A5;
consider y being Element of S1 such that
A8: y >= x and
A9: y in X by A6, WAYBEL_0:def 15;
reconsider f1 = f as Function of S1,T1 ;
f1 . x <= f1 . y by A1, A8, ORDERS_3:def 5;
then A10: b <= f1 . y by A3, A7, ORDERS_2:3;
the carrier of T1 <> {} ;
then dom f = the carrier of S by FUNCT_2:def 1;
then f . y in f .: X by A9, FUNCT_1:def 6;
hence a in downarrow (f .: X) by A10, WAYBEL_0:def 15; :: thesis: verum