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
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)
A3: ( 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;
A4: ( ex_sup_of Y "/\" D,S & f preserves_sup_of {x} "/\" D ) by WAYBEL_0:75, WAYBEL_0:def 33;
reconsider X = f .: D as directed Subset of T by Lm1, YELLOW_2:15;
A5: dom f = the carrier of S by FUNCT_2:def 1;
A6: {(f . x)} "/\" (f .: D) = { ((f . x) "/\" y) where y is Element of T : y in f .: D } by YELLOW_4:42;
A7: {(f . x)} "/\" (f .: D) c= f .: ({x} "/\" D)

proof

let p be object ; :: 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
A8: p = (f . x) "/\" y and
A9: y in f .: D by A6;
consider k being object such that
A10: k in dom f and
A11: k in D and
A12: y = f . k by A9, FUNCT_1:def 6;
reconsider k = k as Element of S by A10;
x "/\" k in { (x "/\" a) where a is Element of S : a in D } by A11;
then A13: x "/\" k in {x} "/\" D by YELLOW_4:42;
f preserves_inf_of {x,k} by A2;
then p = f . (x "/\" k) by A8, A12, YELLOW_3:8;
hence p in f .: ({x} "/\" D) by A5, A13, FUNCT_1:def 6; :: thesis: verum

end;

A14: {x} "/\" D = { (x "/\" y) where y is Element of S : y in D } by YELLOW_4:42;
A15: f .: ({x} "/\" D) c= {(f . x)} "/\" (f .: D)

proof

let p be object ; :: 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 object such that
A16: m in dom f and
A17: m in {x} "/\" D and
A18: p = f . m by FUNCT_1:def 6;
reconsider m = m as Element of S by A16;
consider a being Element of S such that
A19: m = x "/\" a and
A20: a in D by A14, A17;
reconsider fa = f . a as Element of T ;
f preserves_inf_of {x,a} by A2;
then A21: p = (f . x) "/\" fa by A18, A19, YELLOW_3:8;
fa in f .: D by A5, A20, FUNCT_1:def 6;
hence p in {(f . x)} "/\" (f .: D) by A6, A21; :: thesis: verum

end;

f . (x "/\" (sup D)) = (f . x) "/\" (f . (sup D)) by A2, Th1
.= (f . x) "/\" (sup X) by A3
.= sup ({(f . x)} "/\" X) by A1, WAYBEL_2:def 6
.= sup (f .: ({x} "/\" D)) by A7, A15, XBOOLE_0:def 10
.= f . (sup ({x} "/\" D)) by A4 ;
hence x "/\" (sup D) = sup ({x} "/\" D) by A2; :: thesis: verum

end;

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