let S, T be complete LATTICE; :: thesis: for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is one-to-one holds
S is meet-continuous
let f be sups-preserving Function of S,T; :: thesis: ( T is meet-continuous & f is meet-preserving & f is one-to-one implies S is meet-continuous )
assume that
A1: T is meet-continuous and
A2: ( f is meet-preserving & f is one-to-one ) ; :: thesis: S is meet-continuous
A3: T is meet-continuous LATTICE by A1;
S is satisfying_MC

proof

let x be Element of S; :: according to WAYBEL_2:def 6 :: thesis: for b₁ being Element of bool the carrier of S holds x "/\" ("\/" b₁,S) = "\/" ({x} "/\" b₁),S
let D be non empty directed Subset of S; :: thesis: x "/\" ("\/" D,S) = "\/" ({x} "/\" D),S
A4: ( dom f = the carrier of S & rng f c= the carrier of T ) by FUNCT_2:def 1;
A5: ( ex_sup_of D,S & f preserves_sup_of D ) by WAYBEL_0:75, WAYBEL_0:def 33;
reconsider Y = {x} as non empty directed Subset of S by WAYBEL_0:5;
A6: ( ex_sup_of Y "/\" D,S & f preserves_sup_of {x} "/\" D ) by WAYBEL_0:75, WAYBEL_0:def 33;
A7: {(f . x)} "/\" (f .: D) = { ((f . x) "/\" y) where y is Element of T : y in f .: D } by YELLOW_4:42;
A8: {x} "/\" D = { (x "/\" y) where y is Element of S : y in D } by YELLOW_4:42;
A9: {(f . x)} "/\" (f .: D) c= f .: ({x} "/\" D)

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in {(f . x)} "/\" (f .: D) or p in f .: ({x} "/\" D) )
assume p in {(f . x)} "/\" (f .: D) ; :: thesis: p in f .: ({x} "/\" D)
then consider y being Element of T such that
A10: ( p = (f . x) "/\" y & y in f .: D ) by A7;
consider k being set such that
A11: ( k in dom f & k in D & y = f . k ) by A10, FUNCT_1:def 12;
reconsider k = k as Element of S by A11;
f preserves_inf_of {x,k} by A2, WAYBEL_0:def 34;
then A12: p = f . (x "/\" k) by A10, A11, YELLOW_3:8;
x "/\" k in { (x "/\" a) where a is Element of S : a in D } by A11;
then ( x "/\" k in dom f & x "/\" k in {x} "/\" D ) by A4, YELLOW_4:42;
hence p in f .: ({x} "/\" D) by A12, FUNCT_1:def 12; :: thesis: verum

end;

A13: f .: ({x} "/\" D) c= {(f . x)} "/\" (f .: D)

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in f .: ({x} "/\" D) or p in {(f . x)} "/\" (f .: D) )
assume p in f .: ({x} "/\" D) ; :: thesis: p in {(f . x)} "/\" (f .: D)
then consider m being set such that
A14: ( m in dom f & m in {x} "/\" D & p = f . m ) by FUNCT_1:def 12;
reconsider m = m as Element of S by A14;
consider a being Element of S such that
A15: ( m = x "/\" a & a in D ) by A8, A14;
reconsider fa = f . a as Element of T ;
A16: fa in f .: D by A4, A15, FUNCT_1:def 12;
f preserves_inf_of {x,a} by A2, WAYBEL_0:def 34;
then p = (f . x) "/\" fa by A14, A15, YELLOW_3:8;
hence p in {(f . x)} "/\" (f .: D) by A7, A16; :: thesis: verum

end;

reconsider X = f .: D as directed Subset of T by Lm1, YELLOW_2:17;
f . (x "/\" (sup D)) = (f . x) "/\" (f . (sup D)) by A2, Th1
.= (f . x) "/\" (sup X) by A5, WAYBEL_0:def 31
.= sup ({(f . x)} "/\" X) by A3, WAYBEL_2:def 6
.= sup (f .: ({x} "/\" D)) by A9, A13, XBOOLE_0:def 10
.= f . (sup ({x} "/\" D)) by A6, WAYBEL_0:def 31 ;
hence x "/\" (sup D) = sup ({x} "/\" D) by A2, A4, FUNCT_1:def 8; :: thesis: verum

end;

hence S is meet-continuous ; :: thesis: verum