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 set ; :: 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 & fx in f .: (downarrow X) ) by A2, WAYBEL_0:def 15;
consider x being set such that
A4: ( x in dom f & x in downarrow X & fx = f . x ) by A3, FUNCT_1:def 12;
reconsider S1 = S as non empty reflexive RelStr by A4;
reconsider x = x as Element of S1 by A4;
reconsider f1 = f as Function of S1,T1 ;
consider y being Element of S1 such that
A5: ( y >= x & y in X ) by A4, WAYBEL_0:def 15;
f1 . x <= f1 . y by A1, A5, ORDERS_3:def 5;
then A6: b <= f1 . y by A3, A4, ORDERS_2:26;
the carrier of T1 <> {} ;
then dom f = the carrier of S by FUNCT_2:def 1;
then f . y in f .: X by A5, FUNCT_1:def 12;
hence a in downarrow (f .: X) by A6, WAYBEL_0:def 15; :: thesis: verum