let S, T be non empty RelStr ; :: thesis: for D being Subset of S

for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds

f . (inf D) <= inf (f .: D)

let D be Subset of S; :: thesis: for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds

f . (inf D) <= inf (f .: D)

let f be Function of S,T; :: thesis: ( ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone implies f . (inf D) <= inf (f .: D) )

assume A1: ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) ; :: thesis: ( not f is monotone or f . (inf D) <= inf (f .: D) )

A2: ex_inf_of D,S by A1, YELLOW_0:17;

A3: ex_inf_of f .: D,T by A1, YELLOW_0:17;

assume A4: f is monotone ; :: thesis: f . (inf D) <= inf (f .: D)

inf D is_<=_than D by A2, YELLOW_0:def 10;

then f . (inf D) is_<=_than f .: D by A4, YELLOW_2:13;

hence f . (inf D) <= inf (f .: D) by A3, YELLOW_0:def 10; :: thesis: verum

for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds

f . (inf D) <= inf (f .: D)

let D be Subset of S; :: thesis: for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds

f . (inf D) <= inf (f .: D)

let f be Function of S,T; :: thesis: ( ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone implies f . (inf D) <= inf (f .: D) )

assume A1: ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) ; :: thesis: ( not f is monotone or f . (inf D) <= inf (f .: D) )

A2: ex_inf_of D,S by A1, YELLOW_0:17;

A3: ex_inf_of f .: D,T by A1, YELLOW_0:17;

assume A4: f is monotone ; :: thesis: f . (inf D) <= inf (f .: D)

inf D is_<=_than D by A2, YELLOW_0:def 10;

then f . (inf D) is_<=_than f .: D by A4, YELLOW_2:13;

hence f . (inf D) <= inf (f .: D) by A3, YELLOW_0:def 10; :: thesis: verum