let S, T be non empty Poset; :: thesis: for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is monotone
let f be Function of S,T; :: thesis: ( ( for X being Filter of S holds f preserves_inf_of X ) implies f is monotone )
assume A1: for X being Filter of S holds f preserves_inf_of X ; :: thesis: f is monotone
let x, y be Element of S; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) )
A2: ex_inf_of {x},S by YELLOW_0:38;
A3: ex_inf_of {y},S by YELLOW_0:38;
A4: f preserves_inf_of uparrow x by A1;
A5: f preserves_inf_of uparrow y by A1;
A6: ex_inf_of uparrow x,S by A2, Th37;
A7: ex_inf_of uparrow y,S by A3, Th37;
A8: ex_inf_of f .: (uparrow x),T by A4, A6;
A9: ex_inf_of f .: (uparrow y),T by A5, A7;
A10: inf (f .: (uparrow x)) = f . (inf (uparrow x)) by A4, A6;
A11: inf (f .: (uparrow y)) = f . (inf (uparrow y)) by A5, A7;
assume x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ )
then A12: uparrow y c= uparrow x by Th22;
A13: inf (f .: (uparrow x)) = f . (inf {x}) by A10, Th38, YELLOW_0:38;
A14: inf (f .: (uparrow y)) = f . (inf {y}) by A11, Th38, YELLOW_0:38;
A15: inf (f .: (uparrow x)) = f . x by A13, YELLOW_0:39;
inf (f .: (uparrow y)) = f . y by A14, YELLOW_0:39;
hence for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) by A8, A9, A12, A15, RELAT_1:123, YELLOW_0:35; :: thesis: verum