:: WAYBEL20 semantic presentation begin theorem Th1: :: WAYBEL20:1 for X being set for S being Subset of (id X) holds proj1 S = proj2 S proof let X be set ; ::_thesis: for S being Subset of (id X) holds proj1 S = proj2 S let S be Subset of (id X); ::_thesis: proj1 S = proj2 S now__::_thesis:_for_x_being_set_holds_ (_(_x_in_proj1_S_implies_x_in_proj2_S_)_&_(_x_in_proj2_S_implies_x_in_proj1_S_)_) let x be set ; ::_thesis: ( ( x in proj1 S implies x in proj2 S ) & ( x in proj2 S implies x in proj1 S ) ) hereby ::_thesis: ( x in proj2 S implies x in proj1 S ) assume x in proj1 S ; ::_thesis: x in proj2 S then consider y being set such that A1: [x,y] in S by XTUPLE_0:def_12; x = y by A1, RELAT_1:def_10; hence x in proj2 S by A1, XTUPLE_0:def_13; ::_thesis: verum end; assume x in proj2 S ; ::_thesis: x in proj1 S then consider y being set such that A2: [y,x] in S by XTUPLE_0:def_13; x = y by A2, RELAT_1:def_10; hence x in proj1 S by A2, XTUPLE_0:def_12; ::_thesis: verum end; hence proj1 S = proj2 S by TARSKI:1; ::_thesis: verum end; theorem Th2: :: WAYBEL20:2 for X, Y being non empty set for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X proof let X, Y be non empty set ; ::_thesis: for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X let f be Function of X,Y; ::_thesis: [:f,f:] " (id Y) is Equivalence_Relation of X set ff = [:f,f:] " (id Y); A1: dom f = X by FUNCT_2:def_1; reconsider R9 = [:f,f:] " (id Y) as Relation of X ; A2: dom [:f,f:] = [:(dom f),(dom f):] by FUNCT_3:def_8; R9 is_reflexive_in X proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in R9 ) assume A3: x in X ; ::_thesis: [x,x] in R9 then reconsider x9 = x as Element of X ; A4: [(f . x9),(f . x9)] in id Y by RELAT_1:def_10; ( [x,x] in dom [:f,f:] & [(f . x),(f . x)] = [:f,f:] . (x,x) ) by A2, A1, A3, FUNCT_3:def_8, ZFMISC_1:def_2; hence [x,x] in R9 by A4, FUNCT_1:def_7; ::_thesis: verum end; then A5: ( dom R9 = X & field R9 = X ) by ORDERS_1:13; A6: R9 is_symmetric_in X proof let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in X or not y in X or not [x,y] in R9 or [y,x] in R9 ) assume that A7: ( x in X & y in X ) and A8: [x,y] in R9 ; ::_thesis: [y,x] in R9 reconsider x9 = x, y9 = y as Element of X by A7; A9: ( [y,x] in dom [:f,f:] & [(f . y),(f . x)] = [:f,f:] . (y,x) ) by A2, A1, A7, FUNCT_3:def_8, ZFMISC_1:def_2; A10: ( [:f,f:] . [x,y] in id Y & [(f . x),(f . y)] = [:f,f:] . (x,y) ) by A1, A7, A8, FUNCT_1:def_7, FUNCT_3:def_8; then f . x9 = f . y9 by RELAT_1:def_10; hence [y,x] in R9 by A10, A9, FUNCT_1:def_7; ::_thesis: verum end; R9 is_transitive_in X proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in R9 or not [y,z] in R9 or [x,z] in R9 ) assume that A11: x in X and A12: y in X and A13: z in X and A14: [x,y] in R9 and A15: [y,z] in R9 ; ::_thesis: [x,z] in R9 A16: ( [x,z] in dom [:f,f:] & [(f . x),(f . z)] = [:f,f:] . (x,z) ) by A2, A1, A11, A13, FUNCT_3:def_8, ZFMISC_1:def_2; reconsider y9 = y, z9 = z as Element of X by A12, A13; ( [:f,f:] . [y,z] in id Y & [(f . y),(f . z)] = [:f,f:] . (y,z) ) by A1, A12, A13, A15, FUNCT_1:def_7, FUNCT_3:def_8; then A17: f . y9 = f . z9 by RELAT_1:def_10; ( [:f,f:] . [x,y] in id Y & [(f . x),(f . y)] = [:f,f:] . (x,y) ) by A1, A11, A12, A14, FUNCT_1:def_7, FUNCT_3:def_8; hence [x,z] in R9 by A17, A16, FUNCT_1:def_7; ::_thesis: verum end; hence [:f,f:] " (id Y) is Equivalence_Relation of X by A5, A6, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum end; definition let L1, L2, T1, T2 be RelStr ; let f be Function of L1,T1; let g be Function of L2,T2; :: original: [: redefine func[:f,g:] -> Function of [:L1,L2:],[:T1,T2:]; coherence [:f,g:] is Function of [:L1,L2:],[:T1,T2:] proof ( the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] & the carrier of [:T1,T2:] = [: the carrier of T1, the carrier of T2:] ) by YELLOW_3:def_2; hence [:f,g:] is Function of [:L1,L2:],[:T1,T2:] ; ::_thesis: verum end; end; theorem Th3: :: WAYBEL20:3 for f, g being Function for X being set holds ( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) ) proof let f, g be Function; ::_thesis: for X being set holds ( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) ) let X be set ; ::_thesis: ( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) ) A1: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def_8; hereby :: according to TARSKI:def_3 ::_thesis: proj2 ([:f,g:] .: X) c= g .: (proj2 X) let x be set ; ::_thesis: ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) assume x in proj1 ([:f,g:] .: X) ; ::_thesis: x in f .: (proj1 X) then consider y being set such that A2: [x,y] in [:f,g:] .: X by XTUPLE_0:def_12; consider xy being set such that A3: xy in dom [:f,g:] and A4: xy in X and A5: [x,y] = [:f,g:] . xy by A2, FUNCT_1:def_6; consider x9, y9 being set such that A6: x9 in dom f and A7: y9 in dom g and A8: xy = [x9,y9] by A1, A3, ZFMISC_1:def_2; [x,y] = [:f,g:] . (x9,y9) by A5, A8 .= [(f . x9),(g . y9)] by A6, A7, FUNCT_3:def_8 ; then A9: x = f . x9 by XTUPLE_0:1; x9 in proj1 X by A4, A8, XTUPLE_0:def_12; hence x in f .: (proj1 X) by A6, A9, FUNCT_1:def_6; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 ([:f,g:] .: X) or y in g .: (proj2 X) ) assume y in proj2 ([:f,g:] .: X) ; ::_thesis: y in g .: (proj2 X) then consider x being set such that A10: [x,y] in [:f,g:] .: X by XTUPLE_0:def_13; consider xy being set such that A11: xy in dom [:f,g:] and A12: xy in X and A13: [x,y] = [:f,g:] . xy by A10, FUNCT_1:def_6; consider x9, y9 being set such that A14: x9 in dom f and A15: y9 in dom g and A16: xy = [x9,y9] by A1, A11, ZFMISC_1:def_2; [x,y] = [:f,g:] . (x9,y9) by A13, A16 .= [(f . x9),(g . y9)] by A14, A15, FUNCT_3:def_8 ; then A17: y = g . y9 by XTUPLE_0:1; y9 in proj2 X by A12, A16, XTUPLE_0:def_13; hence y in g .: (proj2 X) by A15, A17, FUNCT_1:def_6; ::_thesis: verum end; theorem Th4: :: WAYBEL20:4 for f, g being Function for X being set st X c= [:(dom f),(dom g):] holds ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) ) proof let f, g be Function; ::_thesis: for X being set st X c= [:(dom f),(dom g):] holds ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) ) let X be set ; ::_thesis: ( X c= [:(dom f),(dom g):] implies ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) ) ) assume A1: X c= [:(dom f),(dom g):] ; ::_thesis: ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) ) A2: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def_8; A3: proj1 ([:f,g:] .: X) c= f .: (proj1 X) by Th3; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_proj1_([:f,g:]_.:_X)_implies_x_in_f_.:_(proj1_X)_)_&_(_x_in_f_.:_(proj1_X)_implies_x_in_proj1_([:f,g:]_.:_X)_)_) let x be set ; ::_thesis: ( ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) & ( x in f .: (proj1 X) implies x in proj1 ([:f,g:] .: X) ) ) thus ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) by A3; ::_thesis: ( x in f .: (proj1 X) implies x in proj1 ([:f,g:] .: X) ) assume x in f .: (proj1 X) ; ::_thesis: x in proj1 ([:f,g:] .: X) then consider x9 being set such that A4: x9 in dom f and A5: x9 in proj1 X and A6: x = f . x9 by FUNCT_1:def_6; consider y9 being set such that A7: [x9,y9] in X by A5, XTUPLE_0:def_12; y9 in dom g by A1, A7, ZFMISC_1:87; then [:f,g:] . (x9,y9) = [(f . x9),(g . y9)] by A4, FUNCT_3:def_8; then [x,(g . y9)] in [:f,g:] .: X by A1, A2, A6, A7, FUNCT_1:def_6; hence x in proj1 ([:f,g:] .: X) by XTUPLE_0:def_12; ::_thesis: verum end; hence proj1 ([:f,g:] .: X) = f .: (proj1 X) by TARSKI:1; ::_thesis: proj2 ([:f,g:] .: X) = g .: (proj2 X) A8: proj2 ([:f,g:] .: X) c= g .: (proj2 X) by Th3; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_proj2_([:f,g:]_.:_X)_implies_x_in_g_.:_(proj2_X)_)_&_(_x_in_g_.:_(proj2_X)_implies_x_in_proj2_([:f,g:]_.:_X)_)_) let x be set ; ::_thesis: ( ( x in proj2 ([:f,g:] .: X) implies x in g .: (proj2 X) ) & ( x in g .: (proj2 X) implies x in proj2 ([:f,g:] .: X) ) ) thus ( x in proj2 ([:f,g:] .: X) implies x in g .: (proj2 X) ) by A8; ::_thesis: ( x in g .: (proj2 X) implies x in proj2 ([:f,g:] .: X) ) assume x in g .: (proj2 X) ; ::_thesis: x in proj2 ([:f,g:] .: X) then consider x9 being set such that A9: x9 in dom g and A10: x9 in proj2 X and A11: x = g . x9 by FUNCT_1:def_6; consider y9 being set such that A12: [y9,x9] in X by A10, XTUPLE_0:def_13; y9 in dom f by A1, A12, ZFMISC_1:87; then [:f,g:] . (y9,x9) = [(f . y9),(g . x9)] by A9, FUNCT_3:def_8; then [(f . y9),x] in [:f,g:] .: X by A1, A2, A11, A12, FUNCT_1:def_6; hence x in proj2 ([:f,g:] .: X) by XTUPLE_0:def_13; ::_thesis: verum end; hence proj2 ([:f,g:] .: X) = g .: (proj2 X) by TARSKI:1; ::_thesis: verum end; theorem Th5: :: WAYBEL20:5 for S being non empty antisymmetric RelStr st ex_inf_of {} ,S holds S is upper-bounded proof let S be non empty antisymmetric RelStr ; ::_thesis: ( ex_inf_of {} ,S implies S is upper-bounded ) assume A1: ex_inf_of {} ,S ; ::_thesis: S is upper-bounded take Top S ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of S is_<=_than Top S let x be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not x in the carrier of S or x <= Top S ) {} is_>=_than x by YELLOW_0:6; hence ( not x in the carrier of S or x <= Top S ) by A1, YELLOW_0:31; ::_thesis: verum end; theorem Th6: :: WAYBEL20:6 for S being non empty antisymmetric RelStr st ex_sup_of {} ,S holds S is lower-bounded proof let S be non empty antisymmetric RelStr ; ::_thesis: ( ex_sup_of {} ,S implies S is lower-bounded ) assume A1: ex_sup_of {} ,S ; ::_thesis: S is lower-bounded take Bottom S ; :: according to YELLOW_0:def_4 ::_thesis: Bottom S is_<=_than the carrier of S let x be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not x in the carrier of S or Bottom S <= x ) {} is_<=_than x by YELLOW_0:6; hence ( not x in the carrier of S or Bottom S <= x ) by A1, YELLOW_0:30; ::_thesis: verum end; theorem Th7: :: WAYBEL20:7 for L1, L2 being non empty antisymmetric RelStr for D being Subset of [:L1,L2:] st ex_inf_of D,[:L1,L2:] holds inf D = [(inf (proj1 D)),(inf (proj2 D))] proof let L1, L2 be non empty antisymmetric RelStr ; ::_thesis: for D being Subset of [:L1,L2:] st ex_inf_of D,[:L1,L2:] holds inf D = [(inf (proj1 D)),(inf (proj2 D))] let D be Subset of [:L1,L2:]; ::_thesis: ( ex_inf_of D,[:L1,L2:] implies inf D = [(inf (proj1 D)),(inf (proj2 D))] ) assume A1: ex_inf_of D,[:L1,L2:] ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))] percases ( D <> {} or D = {} ) ; suppose D <> {} ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))] hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A1, YELLOW_3:47; ::_thesis: verum end; supposeA2: D = {} ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))] then ex_inf_of {} ,L2 by A1, FUNCT_5:8, YELLOW_3:42; then A3: L2 is upper-bounded by Th5; ex_inf_of {} ,L1 by A1, A2, FUNCT_5:8, YELLOW_3:42; then L1 is upper-bounded by Th5; hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A1, A3, YELLOW10:6; ::_thesis: verum end; end; end; theorem Th8: :: WAYBEL20:8 for L1, L2 being non empty antisymmetric RelStr for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))] proof let L1, L2 be non empty antisymmetric RelStr ; ::_thesis: for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))] let D be Subset of [:L1,L2:]; ::_thesis: ( ex_sup_of D,[:L1,L2:] implies sup D = [(sup (proj1 D)),(sup (proj2 D))] ) assume A1: ex_sup_of D,[:L1,L2:] ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))] percases ( D <> {} or D = {} ) ; suppose D <> {} ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))] hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A1, YELLOW_3:46; ::_thesis: verum end; supposeA2: D = {} ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))] then ex_sup_of {} ,L2 by A1, FUNCT_5:8, YELLOW_3:41; then A3: L2 is lower-bounded by Th6; ex_sup_of {} ,L1 by A1, A2, FUNCT_5:8, YELLOW_3:41; then L1 is lower-bounded by Th6; hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A1, A3, YELLOW10:5; ::_thesis: verum end; end; end; theorem Th9: :: WAYBEL20:9 for L1, L2, T1, T2 being non empty antisymmetric RelStr for f being Function of L1,T1 for g being Function of L2,T2 st f is infs-preserving & g is infs-preserving holds [:f,g:] is infs-preserving proof let L1, L2, T1, T2 be non empty antisymmetric RelStr ; ::_thesis: for f being Function of L1,T1 for g being Function of L2,T2 st f is infs-preserving & g is infs-preserving holds [:f,g:] is infs-preserving let f be Function of L1,T1; ::_thesis: for g being Function of L2,T2 st f is infs-preserving & g is infs-preserving holds [:f,g:] is infs-preserving let g be Function of L2,T2; ::_thesis: ( f is infs-preserving & g is infs-preserving implies [:f,g:] is infs-preserving ) assume that A1: f is infs-preserving and A2: g is infs-preserving ; ::_thesis: [:f,g:] is infs-preserving let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def_32 ::_thesis: [:f,g:] preserves_inf_of X A3: f preserves_inf_of proj1 X by A1, WAYBEL_0:def_32; A4: g preserves_inf_of proj2 X by A2, WAYBEL_0:def_32; set iX = [:f,g:] .: X; A5: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def_1; assume A6: ex_inf_of X,[:L1,L2:] ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of [:f,g:] .: X,[:T1,T2:] & "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:])) ) then A7: ex_inf_of proj1 X,L1 by YELLOW_3:42; A8: ex_inf_of proj2 X,L2 by A6, YELLOW_3:42; X c= the carrier of [:L1,L2:] ; then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def_2; then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A5, Th4; then A11: ex_inf_of proj2 ([:f,g:] .: X),T2 by A4, A8, WAYBEL_0:def_30; A12: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A5, A9, Th4; then ex_inf_of proj1 ([:f,g:] .: X),T1 by A3, A7, WAYBEL_0:def_30; hence ex_inf_of [:f,g:] .: X,[:T1,T2:] by A11, YELLOW_3:42; ::_thesis: "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:])) hence inf ([:f,g:] .: X) = [(inf (f .: (proj1 X))),(inf (g .: (proj2 X)))] by A12, A10, Th7 .= [(f . (inf (proj1 X))),(inf (g .: (proj2 X)))] by A3, A7, WAYBEL_0:def_30 .= [(f . (inf (proj1 X))),(g . (inf (proj2 X)))] by A4, A8, WAYBEL_0:def_30 .= [:f,g:] . ((inf (proj1 X)),(inf (proj2 X))) by A5, FUNCT_3:def_8 .= [:f,g:] . (inf X) by A6, Th7 ; ::_thesis: verum end; theorem :: WAYBEL20:10 for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr for f being Function of L1,T1 for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds [:f,g:] is filtered-infs-preserving proof let L1, L2, T1, T2 be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of L1,T1 for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds [:f,g:] is filtered-infs-preserving let f be Function of L1,T1; ::_thesis: for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds [:f,g:] is filtered-infs-preserving let g be Function of L2,T2; ::_thesis: ( f is filtered-infs-preserving & g is filtered-infs-preserving implies [:f,g:] is filtered-infs-preserving ) assume that A1: f is filtered-infs-preserving and A2: g is filtered-infs-preserving ; ::_thesis: [:f,g:] is filtered-infs-preserving let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or [:f,g:] preserves_inf_of X ) assume A3: ( not X is empty & X is filtered ) ; ::_thesis: [:f,g:] preserves_inf_of X then ( not proj1 X is empty & proj1 X is filtered ) by YELLOW_3:21, YELLOW_3:24; then A4: f preserves_inf_of proj1 X by A1, WAYBEL_0:def_36; ( not proj2 X is empty & proj2 X is filtered ) by A3, YELLOW_3:21, YELLOW_3:24; then A5: g preserves_inf_of proj2 X by A2, WAYBEL_0:def_36; set iX = [:f,g:] .: X; A6: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def_1; assume A7: ex_inf_of X,[:L1,L2:] ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of [:f,g:] .: X,[:T1,T2:] & "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:])) ) then A8: ex_inf_of proj1 X,L1 by YELLOW_3:42; X c= the carrier of [:L1,L2:] ; then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def_2; then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A6, Th4; A11: ex_inf_of proj2 X,L2 by A7, YELLOW_3:42; then A12: ex_inf_of proj2 ([:f,g:] .: X),T2 by A5, A10, WAYBEL_0:def_30; A13: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A6, A9, Th4; then ex_inf_of proj1 ([:f,g:] .: X),T1 by A4, A8, WAYBEL_0:def_30; hence ex_inf_of [:f,g:] .: X,[:T1,T2:] by A12, YELLOW_3:42; ::_thesis: "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:])) hence inf ([:f,g:] .: X) = [(inf (f .: (proj1 X))),(inf (g .: (proj2 X)))] by A13, A10, Th7 .= [(f . (inf (proj1 X))),(inf (g .: (proj2 X)))] by A4, A8, WAYBEL_0:def_30 .= [(f . (inf (proj1 X))),(g . (inf (proj2 X)))] by A5, A11, WAYBEL_0:def_30 .= [:f,g:] . ((inf (proj1 X)),(inf (proj2 X))) by A6, FUNCT_3:def_8 .= [:f,g:] . (inf X) by A7, Th7 ; ::_thesis: verum end; theorem :: WAYBEL20:11 for L1, L2, T1, T2 being non empty antisymmetric RelStr for f being Function of L1,T1 for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds [:f,g:] is sups-preserving proof let L1, L2, T1, T2 be non empty antisymmetric RelStr ; ::_thesis: for f being Function of L1,T1 for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds [:f,g:] is sups-preserving let f be Function of L1,T1; ::_thesis: for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds [:f,g:] is sups-preserving let g be Function of L2,T2; ::_thesis: ( f is sups-preserving & g is sups-preserving implies [:f,g:] is sups-preserving ) assume that A1: f is sups-preserving and A2: g is sups-preserving ; ::_thesis: [:f,g:] is sups-preserving let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def_33 ::_thesis: [:f,g:] preserves_sup_of X A3: f preserves_sup_of proj1 X by A1, WAYBEL_0:def_33; A4: g preserves_sup_of proj2 X by A2, WAYBEL_0:def_33; set iX = [:f,g:] .: X; A5: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def_1; assume A6: ex_sup_of X,[:L1,L2:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of [:f,g:] .: X,[:T1,T2:] & "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:])) ) then A7: ex_sup_of proj1 X,L1 by YELLOW_3:41; A8: ex_sup_of proj2 X,L2 by A6, YELLOW_3:41; X c= the carrier of [:L1,L2:] ; then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def_2; then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A5, Th4; then A11: ex_sup_of proj2 ([:f,g:] .: X),T2 by A4, A8, WAYBEL_0:def_31; A12: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A5, A9, Th4; then ex_sup_of proj1 ([:f,g:] .: X),T1 by A3, A7, WAYBEL_0:def_31; hence ex_sup_of [:f,g:] .: X,[:T1,T2:] by A11, YELLOW_3:41; ::_thesis: "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:])) hence sup ([:f,g:] .: X) = [(sup (f .: (proj1 X))),(sup (g .: (proj2 X)))] by A12, A10, Th8 .= [(f . (sup (proj1 X))),(sup (g .: (proj2 X)))] by A3, A7, WAYBEL_0:def_31 .= [(f . (sup (proj1 X))),(g . (sup (proj2 X)))] by A4, A8, WAYBEL_0:def_31 .= [:f,g:] . ((sup (proj1 X)),(sup (proj2 X))) by A5, FUNCT_3:def_8 .= [:f,g:] . (sup X) by A6, Th8 ; ::_thesis: verum end; theorem Th12: :: WAYBEL20:12 for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr for f being Function of L1,T1 for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds [:f,g:] is directed-sups-preserving proof let L1, L2, T1, T2 be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of L1,T1 for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds [:f,g:] is directed-sups-preserving let f be Function of L1,T1; ::_thesis: for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds [:f,g:] is directed-sups-preserving let g be Function of L2,T2; ::_thesis: ( f is directed-sups-preserving & g is directed-sups-preserving implies [:f,g:] is directed-sups-preserving ) assume that A1: f is directed-sups-preserving and A2: g is directed-sups-preserving ; ::_thesis: [:f,g:] is directed-sups-preserving let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or [:f,g:] preserves_sup_of X ) assume A3: ( not X is empty & X is directed ) ; ::_thesis: [:f,g:] preserves_sup_of X then ( not proj1 X is empty & proj1 X is directed ) by YELLOW_3:21, YELLOW_3:22; then A4: f preserves_sup_of proj1 X by A1, WAYBEL_0:def_37; ( not proj2 X is empty & proj2 X is directed ) by A3, YELLOW_3:21, YELLOW_3:22; then A5: g preserves_sup_of proj2 X by A2, WAYBEL_0:def_37; set iX = [:f,g:] .: X; A6: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def_1; assume A7: ex_sup_of X,[:L1,L2:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of [:f,g:] .: X,[:T1,T2:] & "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:])) ) then A8: ex_sup_of proj1 X,L1 by YELLOW_3:41; X c= the carrier of [:L1,L2:] ; then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def_2; then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A6, Th4; A11: ex_sup_of proj2 X,L2 by A7, YELLOW_3:41; then A12: ex_sup_of proj2 ([:f,g:] .: X),T2 by A5, A10, WAYBEL_0:def_31; A13: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A6, A9, Th4; then ex_sup_of proj1 ([:f,g:] .: X),T1 by A4, A8, WAYBEL_0:def_31; hence ex_sup_of [:f,g:] .: X,[:T1,T2:] by A12, YELLOW_3:41; ::_thesis: "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:])) hence sup ([:f,g:] .: X) = [(sup (f .: (proj1 X))),(sup (g .: (proj2 X)))] by A13, A10, Th8 .= [(f . (sup (proj1 X))),(sup (g .: (proj2 X)))] by A4, A8, WAYBEL_0:def_31 .= [(f . (sup (proj1 X))),(g . (sup (proj2 X)))] by A5, A11, WAYBEL_0:def_31 .= [:f,g:] . ((sup (proj1 X)),(sup (proj2 X))) by A6, FUNCT_3:def_8 .= [:f,g:] . (sup X) by A7, Th8 ; ::_thesis: verum end; theorem Th13: :: WAYBEL20:13 for L being non empty antisymmetric RelStr for X being Subset of [:L,L:] st X c= id the carrier of L & ex_inf_of X,[:L,L:] holds inf X in id the carrier of L proof let L be non empty antisymmetric RelStr ; ::_thesis: for X being Subset of [:L,L:] st X c= id the carrier of L & ex_inf_of X,[:L,L:] holds inf X in id the carrier of L let X be Subset of [:L,L:]; ::_thesis: ( X c= id the carrier of L & ex_inf_of X,[:L,L:] implies inf X in id the carrier of L ) assume ( X c= id the carrier of L & ex_inf_of X,[:L,L:] ) ; ::_thesis: inf X in id the carrier of L then ( inf X = [(inf (proj1 X)),(inf (proj2 X))] & inf (proj1 X) = inf (proj2 X) ) by Th1, Th7; hence inf X in id the carrier of L by RELAT_1:def_10; ::_thesis: verum end; theorem Th14: :: WAYBEL20:14 for L being non empty antisymmetric RelStr for X being Subset of [:L,L:] st X c= id the carrier of L & ex_sup_of X,[:L,L:] holds sup X in id the carrier of L proof let L be non empty antisymmetric RelStr ; ::_thesis: for X being Subset of [:L,L:] st X c= id the carrier of L & ex_sup_of X,[:L,L:] holds sup X in id the carrier of L let X be Subset of [:L,L:]; ::_thesis: ( X c= id the carrier of L & ex_sup_of X,[:L,L:] implies sup X in id the carrier of L ) assume ( X c= id the carrier of L & ex_sup_of X,[:L,L:] ) ; ::_thesis: sup X in id the carrier of L then ( sup X = [(sup (proj1 X)),(sup (proj2 X))] & sup (proj1 X) = sup (proj2 X) ) by Th1, Th8; hence sup X in id the carrier of L by RELAT_1:def_10; ::_thesis: verum end; theorem Th15: :: WAYBEL20:15 for L, M being non empty RelStr st L,M are_isomorphic & L is reflexive holds M is reflexive proof let L, M be non empty RelStr ; ::_thesis: ( L,M are_isomorphic & L is reflexive implies M is reflexive ) assume that A1: L,M are_isomorphic and A2: L is reflexive ; ::_thesis: M is reflexive let x be Element of M; :: according to YELLOW_0:def_1 ::_thesis: x <= x M,L are_isomorphic by A1, WAYBEL_1:6; then consider f being Function of M,L such that A3: f is isomorphic by WAYBEL_1:def_8; reconsider fx = f . x as Element of L ; fx <= fx by A2, YELLOW_0:def_1; hence x <= x by A3, WAYBEL_0:66; ::_thesis: verum end; theorem Th16: :: WAYBEL20:16 for L, M being non empty RelStr st L,M are_isomorphic & L is transitive holds M is transitive proof let L, M be non empty RelStr ; ::_thesis: ( L,M are_isomorphic & L is transitive implies M is transitive ) assume that A1: L,M are_isomorphic and A2: L is transitive ; ::_thesis: M is transitive M,L are_isomorphic by A1, WAYBEL_1:6; then consider f being Function of M,L such that A3: f is isomorphic by WAYBEL_1:def_8; let x, y, z be Element of M; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume A4: ( x <= y & y <= z ) ; ::_thesis: x <= z reconsider fz = f . z as Element of L ; reconsider fy = f . y as Element of L ; reconsider fx = f . x as Element of L ; ( fx <= fy & fy <= fz ) by A3, A4, WAYBEL_0:66; then fx <= fz by A2, YELLOW_0:def_2; hence x <= z by A3, WAYBEL_0:66; ::_thesis: verum end; theorem Th17: :: WAYBEL20:17 for L, M being non empty RelStr st L,M are_isomorphic & L is antisymmetric holds M is antisymmetric proof let L, M be non empty RelStr ; ::_thesis: ( L,M are_isomorphic & L is antisymmetric implies M is antisymmetric ) assume that A1: L,M are_isomorphic and A2: L is antisymmetric ; ::_thesis: M is antisymmetric M,L are_isomorphic by A1, WAYBEL_1:6; then consider f being Function of M,L such that A3: f is isomorphic by WAYBEL_1:def_8; let x, y be Element of M; :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y ) assume A4: ( x <= y & y <= x ) ; ::_thesis: x = y reconsider fy = f . y as Element of L ; reconsider fx = f . x as Element of L ; ( fx <= fy & fy <= fx ) by A3, A4, WAYBEL_0:66; then ( dom f = the carrier of M & fx = fy ) by A2, FUNCT_2:def_1, YELLOW_0:def_3; hence x = y by A3, FUNCT_1:def_4; ::_thesis: verum end; theorem Th18: :: WAYBEL20:18 for L, M being non empty RelStr st L,M are_isomorphic & L is complete holds M is complete proof let L, M be non empty RelStr ; ::_thesis: ( L,M are_isomorphic & L is complete implies M is complete ) assume that A1: L,M are_isomorphic and A2: L is complete ; ::_thesis: M is complete let X be Subset of M; :: according to LATTICE5:def_2 ::_thesis: ex b1 being Element of the carrier of M st ( b1 is_<=_than X & ( for b2 being Element of the carrier of M holds ( not b2 is_<=_than X or b2 <= b1 ) ) ) M,L are_isomorphic by A1, WAYBEL_1:6; then consider f being Function of M,L such that A3: f is isomorphic by WAYBEL_1:def_8; reconsider fX = f .: X as Subset of L ; consider fa being Element of L such that A4: fa is_<=_than fX and A5: for fb being Element of L st fb is_<=_than fX holds fb <= fa by A2, LATTICE5:def_2; set a = (f ") . fa; A6: rng f = the carrier of L by A3, WAYBEL_0:66; then (f ") . fa in dom f by A3, FUNCT_1:32; then reconsider a = (f ") . fa as Element of M ; A7: fa = f . a by A3, A6, FUNCT_1:35; take a ; ::_thesis: ( a is_<=_than X & ( for b1 being Element of the carrier of M holds ( not b1 is_<=_than X or b1 <= a ) ) ) A8: dom f = the carrier of M by FUNCT_2:def_1; hereby :: according to LATTICE3:def_8 ::_thesis: for b1 being Element of the carrier of M holds ( not b1 is_<=_than X or b1 <= a ) let b be Element of M; ::_thesis: ( b in X implies a <= b ) assume A9: b in X ; ::_thesis: a <= b reconsider fb = f . b as Element of L ; fb in fX by A8, A9, FUNCT_1:def_6; then fa <= fb by A4, LATTICE3:def_8; hence a <= b by A3, A7, WAYBEL_0:66; ::_thesis: verum end; let b be Element of M; ::_thesis: ( not b is_<=_than X or b <= a ) assume A10: b is_<=_than X ; ::_thesis: b <= a reconsider fb = f . b as Element of L ; fb is_<=_than fX proof let fc be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not fc in fX or fb <= fc ) assume fc in fX ; ::_thesis: fb <= fc then consider c being set such that A11: c in dom f and A12: c in X and A13: fc = f . c by FUNCT_1:def_6; reconsider c = c as Element of M by A11; b <= c by A10, A12, LATTICE3:def_8; hence fb <= fc by A3, A13, WAYBEL_0:66; ::_thesis: verum end; then fb <= fa by A5; hence b <= a by A3, A7, WAYBEL_0:66; ::_thesis: verum end; theorem Th19: :: WAYBEL20:19 for L being non empty transitive RelStr for k being Function of L,L st k is infs-preserving holds corestr k is infs-preserving proof let L be non empty transitive RelStr ; ::_thesis: for k being Function of L,L st k is infs-preserving holds corestr k is infs-preserving let k be Function of L,L; ::_thesis: ( k is infs-preserving implies corestr k is infs-preserving ) assume A1: k is infs-preserving ; ::_thesis: corestr k is infs-preserving let X be Subset of L; :: according to WAYBEL_0:def_32 ::_thesis: corestr k preserves_inf_of X assume A2: ex_inf_of X,L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (corestr k) .: X, Image k & "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) ) set f = corestr k; A3: k = corestr k by WAYBEL_1:30; A4: k preserves_inf_of X by A1, WAYBEL_0:def_32; then A5: ex_inf_of k .: X,L by A2, WAYBEL_0:def_30; reconsider fX = (corestr k) .: X as Subset of (Image k) ; dom k = the carrier of L by FUNCT_2:def_1; then ( rng k = the carrier of (Image k) & k . (inf X) in rng k ) by FUNCT_1:def_3, YELLOW_0:def_15; then "/\" (fX,L) is Element of (Image k) by A4, A3, A2, WAYBEL_0:def_30; hence ex_inf_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:63; ::_thesis: "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) inf (k .: X) = k . (inf X) by A4, A2, WAYBEL_0:def_30; hence "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) by A3, A5, YELLOW_0:63; ::_thesis: verum end; theorem :: WAYBEL20:20 for L being non empty transitive RelStr for k being Function of L,L st k is filtered-infs-preserving holds corestr k is filtered-infs-preserving proof let L be non empty transitive RelStr ; ::_thesis: for k being Function of L,L st k is filtered-infs-preserving holds corestr k is filtered-infs-preserving let k be Function of L,L; ::_thesis: ( k is filtered-infs-preserving implies corestr k is filtered-infs-preserving ) assume A1: k is filtered-infs-preserving ; ::_thesis: corestr k is filtered-infs-preserving let X be Subset of L; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or corestr k preserves_inf_of X ) assume ( not X is empty & X is filtered ) ; ::_thesis: corestr k preserves_inf_of X then A2: k preserves_inf_of X by A1, WAYBEL_0:def_36; set f = corestr k; A3: k = corestr k by WAYBEL_1:30; assume A4: ex_inf_of X,L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (corestr k) .: X, Image k & "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) ) then A5: ex_inf_of k .: X,L by A2, WAYBEL_0:def_30; reconsider fX = (corestr k) .: X as Subset of (Image k) ; dom k = the carrier of L by FUNCT_2:def_1; then ( rng k = the carrier of (Image k) & k . (inf X) in rng k ) by FUNCT_1:def_3, YELLOW_0:def_15; then "/\" (fX,L) is Element of (Image k) by A2, A3, A4, WAYBEL_0:def_30; hence ex_inf_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:63; ::_thesis: "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) inf (k .: X) = k . (inf X) by A2, A4, WAYBEL_0:def_30; hence "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) by A3, A5, YELLOW_0:63; ::_thesis: verum end; theorem :: WAYBEL20:21 for L being non empty transitive RelStr for k being Function of L,L st k is sups-preserving holds corestr k is sups-preserving proof let L be non empty transitive RelStr ; ::_thesis: for k being Function of L,L st k is sups-preserving holds corestr k is sups-preserving let k be Function of L,L; ::_thesis: ( k is sups-preserving implies corestr k is sups-preserving ) assume A1: k is sups-preserving ; ::_thesis: corestr k is sups-preserving let X be Subset of L; :: according to WAYBEL_0:def_33 ::_thesis: corestr k preserves_sup_of X assume A2: ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (corestr k) .: X, Image k & "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) ) set f = corestr k; A3: k = corestr k by WAYBEL_1:30; A4: k preserves_sup_of X by A1, WAYBEL_0:def_33; then A5: ex_sup_of k .: X,L by A2, WAYBEL_0:def_31; reconsider fX = (corestr k) .: X as Subset of (Image k) ; dom k = the carrier of L by FUNCT_2:def_1; then ( rng k = the carrier of (Image k) & k . (sup X) in rng k ) by FUNCT_1:def_3, YELLOW_0:def_15; then "\/" (fX,L) is Element of (Image k) by A4, A3, A2, WAYBEL_0:def_31; hence ex_sup_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:64; ::_thesis: "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) sup (k .: X) = k . (sup X) by A4, A2, WAYBEL_0:def_31; hence "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) by A3, A5, YELLOW_0:64; ::_thesis: verum end; theorem Th22: :: WAYBEL20:22 for L being non empty transitive RelStr for k being Function of L,L st k is directed-sups-preserving holds corestr k is directed-sups-preserving proof let L be non empty transitive RelStr ; ::_thesis: for k being Function of L,L st k is directed-sups-preserving holds corestr k is directed-sups-preserving let k be Function of L,L; ::_thesis: ( k is directed-sups-preserving implies corestr k is directed-sups-preserving ) assume A1: k is directed-sups-preserving ; ::_thesis: corestr k is directed-sups-preserving let X be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or corestr k preserves_sup_of X ) assume ( not X is empty & X is directed ) ; ::_thesis: corestr k preserves_sup_of X then A2: k preserves_sup_of X by A1, WAYBEL_0:def_37; set f = corestr k; A3: k = corestr k by WAYBEL_1:30; assume A4: ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (corestr k) .: X, Image k & "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) ) then A5: ex_sup_of k .: X,L by A2, WAYBEL_0:def_31; reconsider fX = (corestr k) .: X as Subset of (Image k) ; dom k = the carrier of L by FUNCT_2:def_1; then ( rng k = the carrier of (Image k) & k . (sup X) in rng k ) by FUNCT_1:def_3, YELLOW_0:def_15; then "\/" (fX,L) is Element of (Image k) by A2, A3, A4, WAYBEL_0:def_31; hence ex_sup_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:64; ::_thesis: "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) sup (k .: X) = k . (sup X) by A2, A4, WAYBEL_0:def_31; hence "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) by A3, A5, YELLOW_0:64; ::_thesis: verum end; theorem Th23: :: WAYBEL20:23 for S, T being non empty reflexive antisymmetric RelStr for f being Function of S,T st f is filtered-infs-preserving holds f is monotone proof let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of S,T st f is filtered-infs-preserving holds f is monotone let f be Function of S,T; ::_thesis: ( f is filtered-infs-preserving implies f is monotone ) assume A1: f is filtered-infs-preserving ; ::_thesis: f is monotone let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) assume A2: x <= y ; ::_thesis: f . x <= f . y A3: dom f = the carrier of S by FUNCT_2:def_1; A4: for b being Element of S st {x,y} is_>=_than b holds x >= b by YELLOW_0:8; A5: x <= x ; then A6: {x,y} is_>=_than x by A2, YELLOW_0:8; then A7: ex_inf_of {x,y},S by A4, YELLOW_0:31; for a, b being Element of S st a in {x,y} & b in {x,y} holds ex z being Element of S st ( z in {x,y} & a >= z & b >= z ) proof let a, b be Element of S; ::_thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of S st ( z in {x,y} & a >= z & b >= z ) ) assume A8: ( a in {x,y} & b in {x,y} ) ; ::_thesis: ex z being Element of S st ( z in {x,y} & a >= z & b >= z ) take x ; ::_thesis: ( x in {x,y} & a >= x & b >= x ) thus x in {x,y} by TARSKI:def_2; ::_thesis: ( a >= x & b >= x ) thus ( a >= x & b >= x ) by A2, A5, A8, TARSKI:def_2; ::_thesis: verum end; then ( {x,y} is filtered & not {x,y} is empty ) by WAYBEL_0:def_2; then A9: f preserves_inf_of {x,y} by A1, WAYBEL_0:def_36; x = inf {x,y} by A6, A4, YELLOW_0:31; then inf (f .: {x,y}) = f . x by A7, A9, WAYBEL_0:def_30; then A10: f . x = inf {(f . x),(f . y)} by A3, FUNCT_1:60; f .: {x,y} = {(f . x),(f . y)} by A3, FUNCT_1:60; then ex_inf_of {(f . x),(f . y)},T by A7, A9, WAYBEL_0:def_30; then {(f . x),(f . y)} is_>=_than f . x by A10, YELLOW_0:def_10; hence f . x <= f . y by YELLOW_0:8; ::_thesis: verum end; theorem Th24: :: WAYBEL20:24 for S, T being non empty RelStr for f being Function of S,T st f is monotone holds for X being Subset of S st X is filtered holds f .: X is filtered proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is monotone holds for X being Subset of S st X is filtered holds f .: X is filtered let f be Function of S,T; ::_thesis: ( f is monotone implies for X being Subset of S st X is filtered holds f .: X is filtered ) assume A1: f is monotone ; ::_thesis: for X being Subset of S st X is filtered holds f .: X is filtered let X be Subset of S; ::_thesis: ( X is filtered implies f .: X is filtered ) assume A2: X is filtered ; ::_thesis: f .: X is filtered let x, y be Element of T; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in f .: X or not y in f .: X or ex b1 being Element of the carrier of T st ( b1 in f .: X & b1 <= x & b1 <= y ) ) assume x in f .: X ; ::_thesis: ( not y in f .: X or ex b1 being Element of the carrier of T st ( b1 in f .: X & b1 <= x & b1 <= y ) ) then consider a being set such that A3: a in the carrier of S and A4: a in X and A5: x = f . a by FUNCT_2:64; assume y in f .: X ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in f .: X & b1 <= x & b1 <= y ) then consider b being set such that A6: b in the carrier of S and A7: b in X and A8: y = f . b by FUNCT_2:64; reconsider a = a, b = b as Element of S by A3, A6; consider c being Element of S such that A9: c in X and A10: ( c <= a & c <= b ) by A2, A4, A7, WAYBEL_0:def_2; take z = f . c; ::_thesis: ( z in f .: X & z <= x & z <= y ) thus z in f .: X by A9, FUNCT_2:35; ::_thesis: ( z <= x & z <= y ) thus ( z <= x & z <= y ) by A1, A5, A8, A10, WAYBEL_1:def_2; ::_thesis: verum end; theorem Th25: :: WAYBEL20:25 for L1, L2, L3 being non empty RelStr for f being Function of L1,L2 for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds g * f is infs-preserving proof let L1, L2, L3 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds g * f is infs-preserving let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds g * f is infs-preserving let g be Function of L2,L3; ::_thesis: ( f is infs-preserving & g is infs-preserving implies g * f is infs-preserving ) assume that A1: f is infs-preserving and A2: g is infs-preserving ; ::_thesis: g * f is infs-preserving set gf = g * f; let X be Subset of L1; :: according to WAYBEL_0:def_32 ::_thesis: g * f preserves_inf_of X assume A3: ex_inf_of X,L1 ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (g * f) .: X,L3 & "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1)) ) set fX = f .: X; set gfX = (g * f) .: X; A4: f preserves_inf_of X by A1, WAYBEL_0:def_32; then A5: ( (g * f) .: X = g .: (f .: X) & ex_inf_of f .: X,L2 ) by A3, RELAT_1:126, WAYBEL_0:def_30; A6: dom f = the carrier of L1 by FUNCT_2:def_1; A7: g preserves_inf_of f .: X by A2, WAYBEL_0:def_32; hence ex_inf_of (g * f) .: X,L3 by A5, WAYBEL_0:def_30; ::_thesis: "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1)) thus inf ((g * f) .: X) = g . (inf (f .: X)) by A7, A5, WAYBEL_0:def_30 .= g . (f . (inf X)) by A3, A4, WAYBEL_0:def_30 .= (g * f) . (inf X) by A6, FUNCT_1:13 ; ::_thesis: verum end; theorem :: WAYBEL20:26 for L1, L2, L3 being non empty reflexive antisymmetric RelStr for f being Function of L1,L2 for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds g * f is filtered-infs-preserving proof let L1, L2, L3 be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2 for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds g * f is filtered-infs-preserving let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds g * f is filtered-infs-preserving let g be Function of L2,L3; ::_thesis: ( f is filtered-infs-preserving & g is filtered-infs-preserving implies g * f is filtered-infs-preserving ) assume that A1: f is filtered-infs-preserving and A2: g is filtered-infs-preserving ; ::_thesis: g * f is filtered-infs-preserving set gf = g * f; let X be Subset of L1; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or g * f preserves_inf_of X ) assume that A3: ( not X is empty & X is filtered ) and A4: ex_inf_of X,L1 ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (g * f) .: X,L3 & "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1)) ) set xx = the Element of X; set fX = f .: X; set gfX = (g * f) .: X; A5: f preserves_inf_of X by A1, A3, WAYBEL_0:def_36; then A6: ( (g * f) .: X = g .: (f .: X) & ex_inf_of f .: X,L2 ) by A4, RELAT_1:126, WAYBEL_0:def_30; the Element of X in X by A3; then f . the Element of X in f .: X by FUNCT_2:35; then ( not f .: X is empty & f .: X is filtered ) by A1, A3, Th23, Th24; then A7: g preserves_inf_of f .: X by A2, WAYBEL_0:def_36; hence ex_inf_of (g * f) .: X,L3 by A6, WAYBEL_0:def_30; ::_thesis: "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1)) A8: dom f = the carrier of L1 by FUNCT_2:def_1; thus inf ((g * f) .: X) = g . (inf (f .: X)) by A7, A6, WAYBEL_0:def_30 .= g . (f . (inf X)) by A4, A5, WAYBEL_0:def_30 .= (g * f) . (inf X) by A8, FUNCT_1:13 ; ::_thesis: verum end; theorem :: WAYBEL20:27 for L1, L2, L3 being non empty RelStr for f being Function of L1,L2 for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds g * f is sups-preserving proof let L1, L2, L3 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds g * f is sups-preserving let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds g * f is sups-preserving let g be Function of L2,L3; ::_thesis: ( f is sups-preserving & g is sups-preserving implies g * f is sups-preserving ) assume that A1: f is sups-preserving and A2: g is sups-preserving ; ::_thesis: g * f is sups-preserving set gf = g * f; let X be Subset of L1; :: according to WAYBEL_0:def_33 ::_thesis: g * f preserves_sup_of X assume A3: ex_sup_of X,L1 ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (g * f) .: X,L3 & "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1)) ) set fX = f .: X; set gfX = (g * f) .: X; A4: f preserves_sup_of X by A1, WAYBEL_0:def_33; then A5: ( (g * f) .: X = g .: (f .: X) & ex_sup_of f .: X,L2 ) by A3, RELAT_1:126, WAYBEL_0:def_31; A6: dom f = the carrier of L1 by FUNCT_2:def_1; A7: g preserves_sup_of f .: X by A2, WAYBEL_0:def_33; hence ex_sup_of (g * f) .: X,L3 by A5, WAYBEL_0:def_31; ::_thesis: "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1)) thus sup ((g * f) .: X) = g . (sup (f .: X)) by A7, A5, WAYBEL_0:def_31 .= g . (f . (sup X)) by A3, A4, WAYBEL_0:def_31 .= (g * f) . (sup X) by A6, FUNCT_1:13 ; ::_thesis: verum end; theorem :: WAYBEL20:28 for L1, L2, L3 being non empty reflexive antisymmetric RelStr for f being Function of L1,L2 for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds g * f is directed-sups-preserving proof let L1, L2, L3 be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2 for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds g * f is directed-sups-preserving let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds g * f is directed-sups-preserving let g be Function of L2,L3; ::_thesis: ( f is directed-sups-preserving & g is directed-sups-preserving implies g * f is directed-sups-preserving ) assume that A1: f is directed-sups-preserving and A2: g is directed-sups-preserving ; ::_thesis: g * f is directed-sups-preserving set gf = g * f; let X be Subset of L1; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or g * f preserves_sup_of X ) assume that A3: ( not X is empty & X is directed ) and A4: ex_sup_of X,L1 ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (g * f) .: X,L3 & "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1)) ) set xx = the Element of X; set fX = f .: X; set gfX = (g * f) .: X; A5: f preserves_sup_of X by A1, A3, WAYBEL_0:def_37; then A6: ( (g * f) .: X = g .: (f .: X) & ex_sup_of f .: X,L2 ) by A4, RELAT_1:126, WAYBEL_0:def_31; the Element of X in X by A3; then f . the Element of X in f .: X by FUNCT_2:35; then ( not f .: X is empty & f .: X is directed ) by A1, A3, WAYBEL17:3, YELLOW_2:15; then A7: g preserves_sup_of f .: X by A2, WAYBEL_0:def_37; hence ex_sup_of (g * f) .: X,L3 by A6, WAYBEL_0:def_31; ::_thesis: "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1)) A8: dom f = the carrier of L1 by FUNCT_2:def_1; thus sup ((g * f) .: X) = g . (sup (f .: X)) by A7, A6, WAYBEL_0:def_31 .= g . (f . (sup X)) by A4, A5, WAYBEL_0:def_31 .= (g * f) . (sup X) by A8, FUNCT_1:13 ; ::_thesis: verum end; begin theorem :: WAYBEL20:29 for I being non empty set for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds product J is lower-bounded proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds product J is lower-bounded let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) implies product J is lower-bounded ) assume A1: for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ; ::_thesis: product J is lower-bounded deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = Bottom (J . \$1); consider f being ManySortedSet of I such that A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5(); A3: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i) let i be Element of I; ::_thesis: f . i is Element of (J . i) f . i = Bottom (J . i) by A2; hence f . i is Element of (J . i) ; ::_thesis: verum end; dom f = I by PARTFUN1:def_2; then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27; take f ; :: according to YELLOW_0:def_4 ::_thesis: f is_<=_than the carrier of (product J) let b be Element of (product J); :: according to LATTICE3:def_8 ::_thesis: ( not b in the carrier of (product J) or f <= b ) assume b in the carrier of (product J) ; ::_thesis: f <= b now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_b_._i let i be Element of I; ::_thesis: f . i <= b . i ( f . i = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2; hence f . i <= b . i by YELLOW_0:44; ::_thesis: verum end; hence f <= b by WAYBEL_3:28; ::_thesis: verum end; theorem :: WAYBEL20:30 for I being non empty set for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds product J is upper-bounded proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds product J is upper-bounded let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) implies product J is upper-bounded ) assume A1: for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ; ::_thesis: product J is upper-bounded deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = Top (J . \$1); consider f being ManySortedSet of I such that A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5(); A3: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i) let i be Element of I; ::_thesis: f . i is Element of (J . i) f . i = Top (J . i) by A2; hence f . i is Element of (J . i) ; ::_thesis: verum end; dom f = I by PARTFUN1:def_2; then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27; take f ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of (product J) is_<=_than f let b be Element of (product J); :: according to LATTICE3:def_9 ::_thesis: ( not b in the carrier of (product J) or b <= f ) assume b in the carrier of (product J) ; ::_thesis: b <= f now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_b_._i let i be Element of I; ::_thesis: f . i >= b . i ( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2; hence f . i >= b . i by YELLOW_0:45; ::_thesis: verum end; hence b <= f by WAYBEL_3:28; ::_thesis: verum end; theorem :: WAYBEL20:31 for I being non empty set for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i) proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i) let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) implies for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i) ) assume A1: for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ; ::_thesis: for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i) deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = Bottom (J . \$1); consider f being ManySortedSet of I such that A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5(); A3: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i) let i be Element of I; ::_thesis: f . i is Element of (J . i) f . i = Bottom (J . i) by A2; hence f . i is Element of (J . i) ; ::_thesis: verum end; dom f = I by PARTFUN1:def_2; then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27; let i be Element of I; ::_thesis: (Bottom (product J)) . i = Bottom (J . i) A4: {} is_<=_than f by YELLOW_0:6; A5: now__::_thesis:_for_c_being_Element_of_(product_J)_st_{}_is_<=_than_c_&_(_for_b_being_Element_of_(product_J)_st_{}_is_<=_than_b_holds_ b_>=_c_)_holds_ c_=_f let c be Element of (product J); ::_thesis: ( {} is_<=_than c & ( for b being Element of (product J) st {} is_<=_than b holds b >= c ) implies c = f ) assume that {} is_<=_than c and A6: for b being Element of (product J) st {} is_<=_than b holds b >= c ; ::_thesis: c = f now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_c_._i let i be Element of I; ::_thesis: f . i <= c . i ( f . i = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2; hence f . i <= c . i by YELLOW_0:44; ::_thesis: verum end; then A7: f <= c by WAYBEL_3:28; for i being Element of I holds J . i is antisymmetric by A1; then A8: product J is antisymmetric by WAYBEL_3:30; c <= f by A6, YELLOW_0:6; hence c = f by A8, A7, YELLOW_0:def_3; ::_thesis: verum end; A9: now__::_thesis:_for_a_being_Element_of_(product_J)_st_{}_is_<=_than_a_holds_ f_<=_a let a be Element of (product J); ::_thesis: ( {} is_<=_than a implies f <= a ) assume {} is_<=_than a ; ::_thesis: f <= a now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_a_._i let i be Element of I; ::_thesis: f . i <= a . i ( f . i = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2; hence f . i <= a . i by YELLOW_0:44; ::_thesis: verum end; hence f <= a by WAYBEL_3:28; ::_thesis: verum end; now__::_thesis:_for_b_being_Element_of_(product_J)_st_{}_is_<=_than_b_holds_ f_<=_b let b be Element of (product J); ::_thesis: ( {} is_<=_than b implies f <= b ) assume {} is_<=_than b ; ::_thesis: f <= b now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_b_._i let i be Element of I; ::_thesis: f . i <= b . i ( f . i = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2; hence f . i <= b . i by YELLOW_0:44; ::_thesis: verum end; hence f <= b by WAYBEL_3:28; ::_thesis: verum end; then ex_sup_of {} , product J by A4, A5, YELLOW_0:def_7; then f = "\/" ({},(product J)) by A4, A9, YELLOW_0:def_9; hence (Bottom (product J)) . i = Bottom (J . i) by A2; ::_thesis: verum end; theorem :: WAYBEL20:32 for I being non empty set for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds for i being Element of I holds (Top (product J)) . i = Top (J . i) proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds for i being Element of I holds (Top (product J)) . i = Top (J . i) let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) implies for i being Element of I holds (Top (product J)) . i = Top (J . i) ) assume A1: for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ; ::_thesis: for i being Element of I holds (Top (product J)) . i = Top (J . i) deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = Top (J . \$1); consider f being ManySortedSet of I such that A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5(); A3: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i) let i be Element of I; ::_thesis: f . i is Element of (J . i) f . i = Top (J . i) by A2; hence f . i is Element of (J . i) ; ::_thesis: verum end; dom f = I by PARTFUN1:def_2; then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27; let i be Element of I; ::_thesis: (Top (product J)) . i = Top (J . i) A4: {} is_>=_than f by YELLOW_0:6; A5: now__::_thesis:_for_c_being_Element_of_(product_J)_st_{}_is_>=_than_c_&_(_for_b_being_Element_of_(product_J)_st_{}_is_>=_than_b_holds_ b_<=_c_)_holds_ c_=_f let c be Element of (product J); ::_thesis: ( {} is_>=_than c & ( for b being Element of (product J) st {} is_>=_than b holds b <= c ) implies c = f ) assume that {} is_>=_than c and A6: for b being Element of (product J) st {} is_>=_than b holds b <= c ; ::_thesis: c = f now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_c_._i let i be Element of I; ::_thesis: f . i >= c . i ( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2; hence f . i >= c . i by YELLOW_0:45; ::_thesis: verum end; then A7: f >= c by WAYBEL_3:28; for i being Element of I holds J . i is antisymmetric by A1; then A8: product J is antisymmetric by WAYBEL_3:30; c >= f by A6, YELLOW_0:6; hence c = f by A8, A7, YELLOW_0:def_3; ::_thesis: verum end; A9: now__::_thesis:_for_a_being_Element_of_(product_J)_st_{}_is_>=_than_a_holds_ f_>=_a let a be Element of (product J); ::_thesis: ( {} is_>=_than a implies f >= a ) assume {} is_>=_than a ; ::_thesis: f >= a now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_a_._i let i be Element of I; ::_thesis: f . i >= a . i ( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2; hence f . i >= a . i by YELLOW_0:45; ::_thesis: verum end; hence f >= a by WAYBEL_3:28; ::_thesis: verum end; now__::_thesis:_for_b_being_Element_of_(product_J)_st_{}_is_>=_than_b_holds_ f_>=_b let b be Element of (product J); ::_thesis: ( {} is_>=_than b implies f >= b ) assume {} is_>=_than b ; ::_thesis: f >= b now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_b_._i let i be Element of I; ::_thesis: f . i >= b . i ( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2; hence f . i >= b . i by YELLOW_0:45; ::_thesis: verum end; hence f >= b by WAYBEL_3:28; ::_thesis: verum end; then ex_inf_of {} , product J by A4, A5, YELLOW_0:def_8; then f = "/\" ({},(product J)) by A4, A9, YELLOW_0:def_10; hence (Top (product J)) . i = Top (J . i) by A2; ::_thesis: verum end; theorem :: WAYBEL20:33 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds product J is continuous proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds product J is continuous let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete continuous LATTICE ) implies product J is continuous ) assume A1: for i being Element of I holds J . i is complete continuous LATTICE ; ::_thesis: product J is continuous A2: for i being Element of I holds J . i is complete LATTICE by A1; set pJ = product J; reconsider pJ9 = product J as complete LATTICE by A2, WAYBEL_3:31; hereby :: according to WAYBEL_3:def_6 ::_thesis: ( product J is up-complete & product J is satisfying_axiom_of_approximation ) let x be Element of (product J); ::_thesis: ( not waybelow x is empty & waybelow x is directed ) reconsider x9 = x as Element of pJ9 ; not waybelow x9 is empty ; hence not waybelow x is empty ; ::_thesis: waybelow x is directed waybelow x9 is directed ; hence waybelow x is directed ; ::_thesis: verum end; pJ9 is up-complete ; hence product J is up-complete ; ::_thesis: product J is satisfying_axiom_of_approximation let x be Element of (product J); :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),(product J)) set swx = sup (waybelow x); now__::_thesis:_(_dom_x_=_I_&_dom_(sup_(waybelow_x))_=_I_&_(_for_i_being_set_st_i_in_I_holds_ x_._i_=_(sup_(waybelow_x))_._i_)_) thus dom x = I by WAYBEL_3:27; ::_thesis: ( dom (sup (waybelow x)) = I & ( for i being set st i in I holds x . i = (sup (waybelow x)) . i ) ) thus dom (sup (waybelow x)) = I by WAYBEL_3:27; ::_thesis: for i being set st i in I holds x . i = (sup (waybelow x)) . i let i be set ; ::_thesis: ( i in I implies x . i = (sup (waybelow x)) . i ) assume i in I ; ::_thesis: x . i = (sup (waybelow x)) . i then reconsider i9 = i as Element of I ; now__::_thesis:_for_a_being_set_holds_ (_(_a_in_pi_((waybelow_x),i9)_implies_a_in_waybelow_(x_._i9)_)_&_(_a_in_waybelow_(x_._i9)_implies_a_in_pi_((waybelow_x),i9)_)_) reconsider K = {i9} as finite Subset of I ; deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = Bottom (J . \$1); let a be set ; ::_thesis: ( ( a in pi ((waybelow x),i9) implies a in waybelow (x . i9) ) & ( a in waybelow (x . i9) implies a in pi ((waybelow x),i9) ) ) consider g being ManySortedSet of I such that A3: for i being Element of I holds g . i = H1(i) from PBOOLE:sch_5(); set f = g +* (i,a); hereby ::_thesis: ( a in waybelow (x . i9) implies a in pi ((waybelow x),i9) ) assume a in pi ((waybelow x),i9) ; ::_thesis: a in waybelow (x . i9) then consider f being Function such that A4: f in waybelow x and A5: a = f . i by CARD_3:def_6; reconsider f = f as Element of (product J) by A4; f << x by A4, WAYBEL_3:7; then f . i9 << x . i9 by A2, WAYBEL_3:33; hence a in waybelow (x . i9) by A5; ::_thesis: verum end; A6: dom g = I by PARTFUN1:def_2; then A7: dom (g +* (i,a)) = I by FUNCT_7:30; assume A8: a in waybelow (x . i9) ; ::_thesis: a in pi ((waybelow x),i9) now__::_thesis:_for_j_being_Element_of_I_holds_(g_+*_(i,a))_._j_is_Element_of_(J_._j) let j be Element of I; ::_thesis: (g +* (i,a)) . b1 is Element of (J . b1) percases ( i9 = j or i9 <> j ) ; suppose i9 = j ; ::_thesis: (g +* (i,a)) . b1 is Element of (J . b1) hence (g +* (i,a)) . j is Element of (J . j) by A8, A6, FUNCT_7:31; ::_thesis: verum end; suppose i9 <> j ; ::_thesis: (g +* (i,a)) . b1 is Element of (J . b1) then (g +* (i,a)) . j = g . j by FUNCT_7:32 .= Bottom (J . j) by A3 ; hence (g +* (i,a)) . j is Element of (J . j) ; ::_thesis: verum end; end; end; then reconsider f = g +* (i,a) as Element of (product J) by A7, WAYBEL_3:27; A9: now__::_thesis:_for_j_being_Element_of_I_holds_f_._j_<<_x_._j let j be Element of I; ::_thesis: f . b1 << x . b1 percases ( i9 = j or i9 <> j ) ; supposeA10: i9 = j ; ::_thesis: f . b1 << x . b1 f . i9 = a by A6, FUNCT_7:31; hence f . j << x . j by A8, A10, WAYBEL_3:7; ::_thesis: verum end; supposeA11: i9 <> j ; ::_thesis: f . b1 << x . b1 A12: J . j is complete LATTICE by A1; f . j = g . j by A11, FUNCT_7:32 .= Bottom (J . j) by A3 ; hence f . j << x . j by A12, WAYBEL_3:4; ::_thesis: verum end; end; end; now__::_thesis:_for_j_being_Element_of_I_st_not_j_in_K_holds_ f_._j_=_Bottom_(J_._j) let j be Element of I; ::_thesis: ( not j in K implies f . j = Bottom (J . j) ) assume not j in K ; ::_thesis: f . j = Bottom (J . j) then j <> i9 by TARSKI:def_1; hence f . j = g . j by FUNCT_7:32 .= Bottom (J . j) by A3 ; ::_thesis: verum end; then f << x by A2, A9, WAYBEL_3:33; then A13: f in waybelow x ; a = f . i9 by A6, FUNCT_7:31; hence a in pi ((waybelow x),i9) by A13, CARD_3:def_6; ::_thesis: verum end; then A14: pi ((waybelow x),i9) = waybelow (x . i9) by TARSKI:1; ( (sup (waybelow x)) . i9 = sup (pi ((waybelow x),i9)) & J . i9 is satisfying_axiom_of_approximation ) by A1, A2, WAYBEL_3:32; hence x . i = (sup (waybelow x)) . i by A14, WAYBEL_3:def_5; ::_thesis: verum end; hence x = "\/" ((waybelow x),(product J)) by FUNCT_1:2; ::_thesis: verum end; begin theorem Th34: :: WAYBEL20:34 for L, T being complete continuous LATTICE for g being CLHomomorphism of L,T for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds subrelstr S is CLSubFrame of [:L,L:] proof let L, T be complete continuous LATTICE; ::_thesis: for g being CLHomomorphism of L,T for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds subrelstr S is CLSubFrame of [:L,L:] let g be CLHomomorphism of L,T; ::_thesis: for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds subrelstr S is CLSubFrame of [:L,L:] let SL be Subset of [:L,L:]; ::_thesis: ( SL = [:g,g:] " (id the carrier of T) implies subrelstr SL is CLSubFrame of [:L,L:] ) assume A1: SL = [:g,g:] " (id the carrier of T) ; ::_thesis: subrelstr SL is CLSubFrame of [:L,L:] set x = the Element of L; A2: dom g = the carrier of L by FUNCT_2:def_1; then A3: [ the Element of L, the Element of L] in [:(dom g),(dom g):] by ZFMISC_1:87; [(g . the Element of L),(g . the Element of L)] in id the carrier of T by RELAT_1:def_10; then ( dom [:g,g:] = [:(dom g),(dom g):] & [:g,g:] . ( the Element of L, the Element of L) in id the carrier of T ) by A2, FUNCT_3:def_8; then reconsider nSL = SL as non empty Subset of [:L,L:] by A1, A3, FUNCT_1:def_7; set pL = [:L,L:]; set pg = [:g,g:]; A4: ( g is infs-preserving & g is directed-sups-preserving ) by WAYBEL16:def_1; A5: the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def_2; A6: not subrelstr nSL is empty ; A7: subrelstr SL is directed-sups-inheriting proof let X be directed Subset of (subrelstr SL); :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,[:L,L:] or "\/" (X,[:L,L:]) in the carrier of (subrelstr SL) ) assume that A8: X <> {} and A9: ex_sup_of X,[:L,L:] ; ::_thesis: "\/" (X,[:L,L:]) in the carrier of (subrelstr SL) reconsider X9 = X as non empty directed Subset of [:L,L:] by A6, A8, YELLOW_2:7; [:g,g:] is directed-sups-preserving by A4, Th12; then [:g,g:] preserves_sup_of X9 by WAYBEL_0:def_37; then A10: sup ([:g,g:] .: X9) = [:g,g:] . (sup X9) by A9, WAYBEL_0:def_31; X c= the carrier of (subrelstr SL) ; then X c= SL by YELLOW_0:def_15; then A11: [:g,g:] .: X c= [:g,g:] .: SL by RELAT_1:123; ( [:g,g:] .: SL c= id the carrier of T & ex_sup_of [:g,g:] .: X9,[:T,T:] ) by A1, FUNCT_1:75, YELLOW_0:17; then A12: sup ([:g,g:] .: X9) in id the carrier of T by A11, Th14, XBOOLE_1:1; consider x, y being set such that A13: ( x in the carrier of L & y in the carrier of L ) and A14: sup X9 = [x,y] by A5, ZFMISC_1:def_2; [x,y] in [:(dom g),(dom g):] by A2, A13, ZFMISC_1:87; then [x,y] in dom [:g,g:] by FUNCT_3:def_8; then [x,y] in [:g,g:] " (id the carrier of T) by A14, A10, A12, FUNCT_1:def_7; hence "\/" (X,[:L,L:]) in the carrier of (subrelstr SL) by A1, A14, YELLOW_0:def_15; ::_thesis: verum end; subrelstr SL is infs-inheriting proof let X be Subset of (subrelstr SL); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,[:L,L:] or "/\" (X,[:L,L:]) in the carrier of (subrelstr SL) ) assume A15: ex_inf_of X,[:L,L:] ; ::_thesis: "/\" (X,[:L,L:]) in the carrier of (subrelstr SL) X c= the carrier of (subrelstr SL) ; then A16: X c= SL by YELLOW_0:def_15; then reconsider X9 = X as Subset of [:L,L:] by XBOOLE_1:1; A17: ( [:g,g:] .: SL c= id the carrier of T & ex_inf_of [:g,g:] .: X9,[:T,T:] ) by A1, FUNCT_1:75, YELLOW_0:17; [:g,g:] is infs-preserving by A4, Th9; then [:g,g:] preserves_inf_of X9 by WAYBEL_0:def_32; then A18: inf ([:g,g:] .: X9) = [:g,g:] . (inf X9) by A15, WAYBEL_0:def_30; [:g,g:] .: X c= [:g,g:] .: SL by A16, RELAT_1:123; then A19: inf ([:g,g:] .: X9) in id the carrier of T by A17, Th13, XBOOLE_1:1; consider x, y being set such that A20: ( x in the carrier of L & y in the carrier of L ) and A21: inf X9 = [x,y] by A5, ZFMISC_1:def_2; [x,y] in [:(dom g),(dom g):] by A2, A20, ZFMISC_1:87; then [x,y] in dom [:g,g:] by FUNCT_3:def_8; then [x,y] in [:g,g:] " (id the carrier of T) by A21, A18, A19, FUNCT_1:def_7; hence "/\" (X,[:L,L:]) in the carrier of (subrelstr SL) by A1, A21, YELLOW_0:def_15; ::_thesis: verum end; hence subrelstr SL is CLSubFrame of [:L,L:] by A7; ::_thesis: verum end; definition let L be RelStr ; let R be Subset of [:L,L:]; assume A1: R is Equivalence_Relation of the carrier of L ; func EqRel R -> Equivalence_Relation of the carrier of L equals :Def1: :: WAYBEL20:def 1 R; correctness coherence R is Equivalence_Relation of the carrier of L; by A1; end; :: deftheorem Def1 defines EqRel WAYBEL20:def_1_:_ for L being RelStr for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L holds EqRel R = R; definition let L be non empty RelStr ; let R be Subset of [:L,L:]; attrR is CLCongruence means :Def2: :: WAYBEL20:def 2 ( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] ); end; :: deftheorem Def2 defines CLCongruence WAYBEL20:def_2_:_ for L being non empty RelStr for R being Subset of [:L,L:] holds ( R is CLCongruence iff ( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] ) ); theorem Th35: :: WAYBEL20:35 for L being complete LATTICE for R being non empty Subset of [:L,L:] st R is CLCongruence holds for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R proof let L be complete LATTICE; ::_thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R let R be non empty Subset of [:L,L:]; ::_thesis: ( R is CLCongruence implies for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R ) assume A1: R is CLCongruence ; ::_thesis: for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R let x be Element of L; ::_thesis: [(inf (Class ((EqRel R),x))),x] in R set CRx = Class ((EqRel R),x); reconsider SR = [:(Class ((EqRel R),x)),{x}:] as Subset of [:L,L:] ; R is Equivalence_Relation of the carrier of L by A1, Def2; then A2: R = EqRel R by Def1; SR c= the carrier of (subrelstr R) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SR or a in the carrier of (subrelstr R) ) assume a in SR ; ::_thesis: a in the carrier of (subrelstr R) then consider a1, a2 being set such that A3: a1 in Class ((EqRel R),x) and A4: a2 in {x} and A5: a = [a1,a2] by ZFMISC_1:def_2; a2 = x by A4, TARSKI:def_1; then a in R by A2, A3, A5, EQREL_1:19; hence a in the carrier of (subrelstr R) by YELLOW_0:def_15; ::_thesis: verum end; then reconsider SR9 = SR as Subset of (subrelstr R) ; A6: ex_inf_of SR,[:L,L:] by YELLOW_0:17; subrelstr R is CLSubFrame of [:L,L:] by A1, Def2; then A7: "/\" (SR9,[:L,L:]) in the carrier of (subrelstr R) by A6, YELLOW_0:def_18; A8: x in Class ((EqRel R),x) by EQREL_1:20; inf SR = [(inf (proj1 SR)),(inf (proj2 SR))] by Th7, YELLOW_0:17 .= [(inf (Class ((EqRel R),x))),(inf (proj2 SR))] by FUNCT_5:9 .= [(inf (Class ((EqRel R),x))),(inf {x})] by A8, FUNCT_5:9 .= [(inf (Class ((EqRel R),x))),x] by YELLOW_0:39 ; hence [(inf (Class ((EqRel R),x))),x] in R by A7, YELLOW_0:def_15; ::_thesis: verum end; definition let L be complete LATTICE; let R be non empty Subset of [:L,L:]; assume B1: R is CLCongruence ; func kernel_op R -> kernel Function of L,L means :Def3: :: WAYBEL20:def 3 for x being Element of L holds it . x = inf (Class ((EqRel R),x)); existence ex b1 being kernel Function of L,L st for x being Element of L holds b1 . x = inf (Class ((EqRel R),x)) proof deffunc H1( Element of L) -> Element of the carrier of L = inf (Class ((EqRel R),\$1)); consider k being Function of the carrier of L, the carrier of L such that A1: for x being Element of L holds k . x = H1(x) from FUNCT_2:sch_4(); reconsider k = k as Function of L,L ; R is Equivalence_Relation of the carrier of L by B1, Def2; then A2: R = EqRel R by Def1; A3: subrelstr R is CLSubFrame of [:L,L:] by B1, Def2; A4: k is monotone proof let x, y be Element of L; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or k . x <= k . y ) assume A5: x <= y ; ::_thesis: k . x <= k . y set CRy = Class ((EqRel R),y); set CRx = Class ((EqRel R),x); reconsider SR = {[(inf (Class ((EqRel R),x))),x],[(inf (Class ((EqRel R),y))),y]} as Subset of [:L,L:] ; A6: inf SR = [(inf (proj1 SR)),(inf (proj2 SR))] by Th7, YELLOW_0:17 .= [(inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))}),(inf (proj2 SR))] by FUNCT_5:13 .= [(inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))}),(inf {x,y})] by FUNCT_5:13 ; ( [(inf (Class ((EqRel R),x))),x] in R & [(inf (Class ((EqRel R),y))),y] in R ) by B1, Th35; then SR c= R by ZFMISC_1:32; then reconsider SR9 = SR as Subset of (subrelstr R) by YELLOW_0:def_15; ex_inf_of SR,[:L,L:] by YELLOW_0:17; then A7: "/\" (SR9,[:L,L:]) in the carrier of (subrelstr R) by A3, YELLOW_0:def_18; inf {x,y} = x "/\" y by YELLOW_0:40 .= x by A5, YELLOW_0:25 ; then [(inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))}),x] in R by A6, A7, YELLOW_0:def_15; then inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} in Class ((EqRel R),x) by A2, EQREL_1:19; then A8: inf (Class ((EqRel R),x)) <= inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} by YELLOW_2:22; inf (Class ((EqRel R),y)) in {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} by TARSKI:def_2; then A9: inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} <= inf (Class ((EqRel R),y)) by YELLOW_2:22; ( k . x = inf (Class ((EqRel R),x)) & k . y = inf (Class ((EqRel R),y)) ) by A1; hence k . x <= k . y by A8, A9, YELLOW_0:def_2; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_L_holds_(k_*_k)_._x_=_k_._x let x be Element of L; ::_thesis: (k * k) . x = k . x set CRx = Class ((EqRel R),x); [(inf (Class ((EqRel R),x))),x] in R by B1, Th35; then inf (Class ((EqRel R),x)) in Class ((EqRel R),x) by A2, EQREL_1:19; then A10: Class ((EqRel R),(inf (Class ((EqRel R),x)))) = Class ((EqRel R),x) by EQREL_1:23; A11: k . x = inf (Class ((EqRel R),x)) by A1; then k . (k . x) = inf (Class ((EqRel R),(inf (Class ((EqRel R),x))))) by A1; hence (k * k) . x = k . x by A11, A10, FUNCT_2:15; ::_thesis: verum end; then k * k = k by FUNCT_2:63; then k is idempotent by QUANTAL1:def_9; then A12: k is projection by A4, WAYBEL_1:def_13; now__::_thesis:_for_x_being_Element_of_L_holds_k_._x_<=_(id_L)_._x let x be Element of L; ::_thesis: k . x <= (id L) . x set CRx = Class ((EqRel R),x); ( x in Class ((EqRel R),x) & inf (Class ((EqRel R),x)) is_<=_than Class ((EqRel R),x) ) by EQREL_1:20, YELLOW_0:33; then A13: inf (Class ((EqRel R),x)) <= x by LATTICE3:def_8; k . x = inf (Class ((EqRel R),x)) by A1; hence k . x <= (id L) . x by A13, FUNCT_1:18; ::_thesis: verum end; then k <= id L by YELLOW_2:9; then reconsider k = k as kernel Function of L,L by A12, WAYBEL_1:def_15; take k ; ::_thesis: for x being Element of L holds k . x = inf (Class ((EqRel R),x)) thus for x being Element of L holds k . x = inf (Class ((EqRel R),x)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being kernel Function of L,L st ( for x being Element of L holds b1 . x = inf (Class ((EqRel R),x)) ) & ( for x being Element of L holds b2 . x = inf (Class ((EqRel R),x)) ) holds b1 = b2 proof let it1, it2 be kernel Function of L,L; ::_thesis: ( ( for x being Element of L holds it1 . x = inf (Class ((EqRel R),x)) ) & ( for x being Element of L holds it2 . x = inf (Class ((EqRel R),x)) ) implies it1 = it2 ) assume that A14: for x being Element of L holds it1 . x = inf (Class ((EqRel R),x)) and A15: for x being Element of L holds it2 . x = inf (Class ((EqRel R),x)) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_ it1_._x_=_it2_._x let x be set ; ::_thesis: ( x in the carrier of L implies it1 . x = it2 . x ) assume x in the carrier of L ; ::_thesis: it1 . x = it2 . x then reconsider x9 = x as Element of L ; thus it1 . x = inf (Class ((EqRel R),x9)) by A14 .= it2 . x by A15 ; ::_thesis: verum end; hence it1 = it2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def3 defines kernel_op WAYBEL20:def_3_:_ for L being complete LATTICE for R being non empty Subset of [:L,L:] st R is CLCongruence holds for b3 being kernel Function of L,L holds ( b3 = kernel_op R iff for x being Element of L holds b3 . x = inf (Class ((EqRel R),x)) ); theorem Th36: :: WAYBEL20:36 for L being complete LATTICE for R being non empty Subset of [:L,L:] st R is CLCongruence holds ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) proof let L be complete LATTICE; ::_thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) let R be non empty Subset of [:L,L:]; ::_thesis: ( R is CLCongruence implies ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) ) set k = kernel_op R; set cL = the carrier of L; A1: dom (kernel_op R) = the carrier of L by FUNCT_2:def_1; assume A2: R is CLCongruence ; ::_thesis: ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) then A3: R is Equivalence_Relation of the carrier of L by Def2; then A4: EqRel R = R by Def1; A5: subrelstr R is CLSubFrame of [:L,L:] by A2, Def2; thus kernel_op R is directed-sups-preserving ::_thesis: R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) proof let D be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or kernel_op R preserves_sup_of D ) assume that A6: ( not D is empty & D is directed ) and ex_sup_of D,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (kernel_op R) .: D,L & "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L)) ) consider e being set such that A7: e in D by A6, XBOOLE_0:def_1; set S = { [((kernel_op R) . x),x] where x is Element of L : x in D } ; A8: { [((kernel_op R) . x),x] where x is Element of L : x in D } c= R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [((kernel_op R) . x),x] where x is Element of L : x in D } or x in R ) assume x in { [((kernel_op R) . x),x] where x is Element of L : x in D } ; ::_thesis: x in R then consider a being Element of L such that A9: x = [((kernel_op R) . a),a] and a in D ; (kernel_op R) . a = inf (Class ((EqRel R),a)) by A2, Def3; hence x in R by A2, A9, Th35; ::_thesis: verum end; then reconsider S9 = { [((kernel_op R) . x),x] where x is Element of L : x in D } as Subset of (subrelstr R) by YELLOW_0:def_15; reconsider S = { [((kernel_op R) . x),x] where x is Element of L : x in D } as Subset of [:L,L:] by A8, XBOOLE_1:1; thus ex_sup_of (kernel_op R) .: D,L by YELLOW_0:17; ::_thesis: "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L)) set d = sup D; set ds = sup ((kernel_op R) .: D); A10: ( the carrier of (subrelstr R) = R & ex_sup_of S,[:L,L:] ) by YELLOW_0:17, YELLOW_0:def_15; reconsider e = e as Element of L by A7; A11: [((kernel_op R) . e),e] in S by A7; A12: S9 is directed proof let x, y be Element of (subrelstr R); :: according to WAYBEL_0:def_1 ::_thesis: ( not x in S9 or not y in S9 or ex b1 being Element of the carrier of (subrelstr R) st ( b1 in S9 & x <= b1 & y <= b1 ) ) assume that A13: x in S9 and A14: y in S9 ; ::_thesis: ex b1 being Element of the carrier of (subrelstr R) st ( b1 in S9 & x <= b1 & y <= b1 ) consider a being Element of L such that A15: x = [((kernel_op R) . a),a] and A16: a in D by A13; consider b being Element of L such that A17: y = [((kernel_op R) . b),b] and A18: b in D by A14; consider c being Element of L such that A19: c in D and A20: a <= c and A21: b <= c by A6, A16, A18, WAYBEL_0:def_1; set z = [((kernel_op R) . c),c]; [((kernel_op R) . c),c] in S9 by A19; then reconsider z = [((kernel_op R) . c),c] as Element of (subrelstr R) ; take z ; ::_thesis: ( z in S9 & x <= z & y <= z ) thus z in S9 by A19; ::_thesis: ( x <= z & y <= z ) (kernel_op R) . a <= (kernel_op R) . c by A20, WAYBEL_1:def_2; then [((kernel_op R) . a),a] <= [((kernel_op R) . c),c] by A20, YELLOW_3:11; hence x <= z by A15, YELLOW_0:60; ::_thesis: y <= z (kernel_op R) . b <= (kernel_op R) . c by A21, WAYBEL_1:def_2; then [((kernel_op R) . b),b] <= [((kernel_op R) . c),c] by A21, YELLOW_3:11; hence y <= z by A17, YELLOW_0:60; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_proj1_S_implies_x_in_(kernel_op_R)_.:_D_)_&_(_x_in_(kernel_op_R)_.:_D_implies_x_in_proj1_S_)_) let x be set ; ::_thesis: ( ( x in proj1 S implies x in (kernel_op R) .: D ) & ( x in (kernel_op R) .: D implies x in proj1 S ) ) hereby ::_thesis: ( x in (kernel_op R) .: D implies x in proj1 S ) assume x in proj1 S ; ::_thesis: x in (kernel_op R) .: D then consider y being set such that A22: [x,y] in S by XTUPLE_0:def_12; consider a being Element of L such that A23: [x,y] = [((kernel_op R) . a),a] and A24: a in D by A22; x = (kernel_op R) . a by A23, XTUPLE_0:1; hence x in (kernel_op R) .: D by A1, A24, FUNCT_1:def_6; ::_thesis: verum end; assume x in (kernel_op R) .: D ; ::_thesis: x in proj1 S then consider y being set such that A25: y in dom (kernel_op R) and A26: y in D and A27: x = (kernel_op R) . y by FUNCT_1:def_6; reconsider y = y as Element of L by A25; [((kernel_op R) . y),y] in S by A26; hence x in proj1 S by A27, XTUPLE_0:def_12; ::_thesis: verum end; then A28: proj1 S = (kernel_op R) .: D by TARSKI:1; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_proj2_S_implies_x_in_D_)_&_(_x_in_D_implies_x_in_proj2_S_)_) let x be set ; ::_thesis: ( ( x in proj2 S implies x in D ) & ( x in D implies x in proj2 S ) ) hereby ::_thesis: ( x in D implies x in proj2 S ) assume x in proj2 S ; ::_thesis: x in D then consider y being set such that A29: [y,x] in S by XTUPLE_0:def_13; ex a being Element of L st ( [y,x] = [((kernel_op R) . a),a] & a in D ) by A29; hence x in D by XTUPLE_0:1; ::_thesis: verum end; assume A30: x in D ; ::_thesis: x in proj2 S then reconsider x9 = x as Element of L ; [((kernel_op R) . x9),x9] in S by A30; hence x in proj2 S by XTUPLE_0:def_13; ::_thesis: verum end; then proj2 S = D by TARSKI:1; then sup S = [(sup ((kernel_op R) .: D)),(sup D)] by A28, Th8, YELLOW_0:17; then [(sup ((kernel_op R) .: D)),(sup D)] in R by A5, A10, A11, A12, WAYBEL_0:def_4; then A31: sup ((kernel_op R) .: D) in Class ((EqRel R),(sup D)) by A4, EQREL_1:19; (kernel_op R) .: D is_<=_than (kernel_op R) . (sup D) proof let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in (kernel_op R) .: D or b <= (kernel_op R) . (sup D) ) assume b in (kernel_op R) .: D ; ::_thesis: b <= (kernel_op R) . (sup D) then consider a being set such that A32: a in dom (kernel_op R) and A33: a in D and A34: b = (kernel_op R) . a by FUNCT_1:def_6; reconsider a = a as Element of L by A32; D is_<=_than sup D by YELLOW_0:32; then a <= sup D by A33, LATTICE3:def_9; hence b <= (kernel_op R) . (sup D) by A34, WAYBEL_1:def_2; ::_thesis: verum end; then A35: sup ((kernel_op R) .: D) <= (kernel_op R) . (sup D) by YELLOW_0:32; (kernel_op R) . (sup D) = inf (Class ((EqRel R),(sup D))) by A2, Def3; then (kernel_op R) . (sup D) <= sup ((kernel_op R) .: D) by A31, YELLOW_2:22; hence "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L)) by A35, YELLOW_0:def_3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_R_implies_x_in_[:(kernel_op_R),(kernel_op_R):]_"_(id_the_carrier_of_L)_)_&_(_x_in_[:(kernel_op_R),(kernel_op_R):]_"_(id_the_carrier_of_L)_implies_x_in_R_)_) let x be set ; ::_thesis: ( ( x in R implies x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) & ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R ) ) hereby ::_thesis: ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R ) assume A36: x in R ; ::_thesis: x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) then x in the carrier of [:L,L:] ; then x in [: the carrier of L, the carrier of L:] by YELLOW_3:def_2; then consider x1, x2 being set such that A37: ( x1 in the carrier of L & x2 in the carrier of L ) and A38: x = [x1,x2] by ZFMISC_1:def_2; reconsider x1 = x1, x2 = x2 as Element of L by A37; A39: ( (kernel_op R) . x1 = inf (Class ((EqRel R),x1)) & (kernel_op R) . x2 = inf (Class ((EqRel R),x2)) ) by A2, Def3; x1 in Class ((EqRel R),x2) by A4, A36, A38, EQREL_1:19; then (kernel_op R) . x1 = (kernel_op R) . x2 by A39, EQREL_1:23; then A40: [((kernel_op R) . x1),((kernel_op R) . x2)] in id the carrier of L by RELAT_1:def_10; dom [:(kernel_op R),(kernel_op R):] = [:(dom (kernel_op R)),(dom (kernel_op R)):] by FUNCT_3:def_8; then A41: [x1,x2] in dom [:(kernel_op R),(kernel_op R):] by A1, ZFMISC_1:87; [:(kernel_op R),(kernel_op R):] . (x1,x2) = [((kernel_op R) . x1),((kernel_op R) . x2)] by A1, FUNCT_3:def_8; hence x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) by A38, A40, A41, FUNCT_1:def_7; ::_thesis: verum end; assume A42: x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ; ::_thesis: x in R then A43: [:(kernel_op R),(kernel_op R):] . x in id the carrier of L by FUNCT_1:def_7; x in dom [:(kernel_op R),(kernel_op R):] by A42, FUNCT_1:def_7; then x in [:(dom (kernel_op R)),(dom (kernel_op R)):] by FUNCT_3:def_8; then consider x1, x2 being set such that A44: ( x1 in dom (kernel_op R) & x2 in dom (kernel_op R) ) and A45: x = [x1,x2] by ZFMISC_1:def_2; reconsider x1 = x1, x2 = x2 as Element of L by A44; [:(kernel_op R),(kernel_op R):] . (x1,x2) = [((kernel_op R) . x1),((kernel_op R) . x2)] by A44, FUNCT_3:def_8; then A46: (kernel_op R) . x1 = (kernel_op R) . x2 by A43, A45, RELAT_1:def_10; (kernel_op R) . x1 = inf (Class ((EqRel R),x1)) by A2, Def3; then [((kernel_op R) . x1),x1] in R by A2, Th35; then A47: [x1,((kernel_op R) . x1)] in R by A3, EQREL_1:6; (kernel_op R) . x2 = inf (Class ((EqRel R),x2)) by A2, Def3; then [((kernel_op R) . x2),x2] in R by A2, Th35; hence x in R by A3, A45, A46, A47, EQREL_1:7; ::_thesis: verum end; hence R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) by TARSKI:1; ::_thesis: verum end; theorem Th37: :: WAYBEL20:37 for L being complete continuous LATTICE for R being Subset of [:L,L:] for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds ex LR being strict complete continuous LATTICE st ( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) proof let L be complete continuous LATTICE; ::_thesis: for R being Subset of [:L,L:] for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds ex LR being strict complete continuous LATTICE st ( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) let R be Subset of [:L,L:]; ::_thesis: for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds ex LR being strict complete continuous LATTICE st ( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) let k be kernel Function of L,L; ::_thesis: ( k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) implies ex LR being strict complete continuous LATTICE st ( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) ) assume that A1: k is directed-sups-preserving and A2: R = [:k,k:] " (id the carrier of L) ; ::_thesis: ex LR being strict complete continuous LATTICE st ( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) set ER = EqRel R; R is Equivalence_Relation of the carrier of L by A2, Th2; then A3: EqRel R = R by Def1; reconsider rngk = rng k as non empty set ; defpred S1[ set , set ] means ex x, y being Element of L st ( \$1 = Class ((EqRel R),x) & \$2 = Class ((EqRel R),y) & k . x <= k . y ); set xx = the Element of L; set cL = the carrier of L; Class ((EqRel R), the Element of L) in Class (EqRel R) by EQREL_1:def_3; then reconsider CER = Class (EqRel R) as non empty Subset-Family of the carrier of L ; consider LR being non empty strict RelStr such that A4: the carrier of LR = CER and A5: for a, b being Element of LR holds ( a <= b iff S1[a,b] ) from YELLOW_0:sch_1(); defpred S2[ set , set ] means ex a being Element of the carrier of L st ( \$1 = Class ((EqRel R),a) & \$2 = k . a ); A6: dom k = the carrier of L by FUNCT_2:def_1; A7: for x being Element of CER ex y being Element of rngk st S2[x,y] proof let x be Element of CER; ::_thesis: ex y being Element of rngk st S2[x,y] consider y being set such that A8: y in the carrier of L and A9: x = Class ((EqRel R),y) by EQREL_1:def_3; reconsider y = y as Element of L by A8; reconsider ky = k . y as Element of rngk by A6, FUNCT_1:def_3; take ky ; ::_thesis: S2[x,ky] thus S2[x,ky] by A9; ::_thesis: verum end; consider f being Function of CER,rngk such that A10: for x being Element of CER holds S2[x,f . x] from FUNCT_2:sch_3(A7); A11: dom [:k,k:] = [: the carrier of L, the carrier of L:] by A6, FUNCT_3:def_8; A12: for a, b being Element of the carrier of L holds ( Class ((EqRel R),a) = Class ((EqRel R),b) iff k . a = k . b ) proof let a, b be Element of the carrier of L; ::_thesis: ( Class ((EqRel R),a) = Class ((EqRel R),b) iff k . a = k . b ) hereby ::_thesis: ( k . a = k . b implies Class ((EqRel R),a) = Class ((EqRel R),b) ) assume Class ((EqRel R),a) = Class ((EqRel R),b) ; ::_thesis: k . a = k . b then a in Class ((EqRel R),b) by EQREL_1:23; then [a,b] in R by A3, EQREL_1:19; then [:k,k:] . (a,b) in id the carrier of L by A2, FUNCT_1:def_7; then [(k . a),(k . b)] in id the carrier of L by A6, FUNCT_3:def_8; hence k . a = k . b by RELAT_1:def_10; ::_thesis: verum end; assume k . a = k . b ; ::_thesis: Class ((EqRel R),a) = Class ((EqRel R),b) then [(k . a),(k . b)] in id the carrier of L by RELAT_1:def_10; then ( [a,b] in [: the carrier of L, the carrier of L:] & [:k,k:] . (a,b) in id the carrier of L ) by A6, FUNCT_3:def_8, ZFMISC_1:def_2; then [a,b] in EqRel R by A2, A3, A11, FUNCT_1:def_7; then a in Class ((EqRel R),b) by EQREL_1:19; hence Class ((EqRel R),a) = Class ((EqRel R),b) by EQREL_1:23; ::_thesis: verum end; A13: for x being Element of L holds f . (Class ((EqRel R),x)) = k . x proof let x be Element of L; ::_thesis: f . (Class ((EqRel R),x)) = k . x reconsider CERx = Class ((EqRel R),x) as Element of CER by EQREL_1:def_3; ex a being Element of the carrier of L st ( CERx = Class ((EqRel R),a) & f . CERx = k . a ) by A10; hence f . (Class ((EqRel R),x)) = k . x by A12; ::_thesis: verum end; A14: for x being Element of LR ex a being Element of L st x = Class ((EqRel R),a) proof let x be Element of LR; ::_thesis: ex a being Element of L st x = Class ((EqRel R),a) x in CER by A4; then consider a being set such that A15: a in the carrier of L and A16: x = Class ((EqRel R),a) by EQREL_1:def_3; reconsider a = a as Element of L by A15; take a ; ::_thesis: x = Class ((EqRel R),a) thus x = Class ((EqRel R),a) by A16; ::_thesis: verum end; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_CER_&_x2_in_CER_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in CER & x2 in CER & f . x1 = f . x2 implies x1 = x2 ) assume that A17: x1 in CER and A18: x2 in CER and A19: f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider x19 = x1 as Element of LR by A4, A17; consider a being Element of L such that A20: x19 = Class ((EqRel R),a) by A14; reconsider x29 = x2 as Element of LR by A4, A18; consider b being Element of L such that A21: x29 = Class ((EqRel R),b) by A14; A22: f . x29 = k . b by A13, A21; f . x19 = k . a by A13, A20; hence x1 = x2 by A12, A19, A20, A21, A22; ::_thesis: verum end; then A23: f is one-to-one by FUNCT_2:19; set tIR = the InternalRel of LR; A24: dom f = CER by FUNCT_2:def_1; reconsider f = f as Function of LR,(Image k) by A4, YELLOW_0:def_15; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_f_implies_y_in_rngk_)_&_(_y_in_rngk_implies_y_in_rng_f_)_) let y be set ; ::_thesis: ( ( y in rng f implies y in rngk ) & ( y in rngk implies y in rng f ) ) hereby ::_thesis: ( y in rngk implies y in rng f ) assume y in rng f ; ::_thesis: y in rngk then consider x being set such that A25: x in dom f and A26: y = f . x by FUNCT_1:def_3; reconsider x = x as Element of LR by A25; consider a being Element of L such that A27: x = Class ((EqRel R),a) by A14; f . x = k . a by A13, A27; hence y in rngk by A6, A26, FUNCT_1:def_3; ::_thesis: verum end; assume y in rngk ; ::_thesis: y in rng f then consider x being set such that A28: x in dom k and A29: y = k . x by FUNCT_1:def_3; reconsider x = x as Element of L by A28; ( Class ((EqRel R),x) in CER & f . (Class ((EqRel R),x)) = k . x ) by A13, EQREL_1:def_3; hence y in rng f by A24, A29, FUNCT_1:def_3; ::_thesis: verum end; then A30: ( the carrier of (Image k) = rngk & rng f = rngk ) by TARSKI:1, YELLOW_0:def_15; for x, y being Element of LR holds ( x <= y iff f . x <= f . y ) proof let x, y be Element of LR; ::_thesis: ( x <= y iff f . x <= f . y ) x in CER by A4; then consider a being set such that A31: a in the carrier of L and A32: x = Class ((EqRel R),a) by EQREL_1:def_3; hereby ::_thesis: ( f . x <= f . y implies x <= y ) assume x <= y ; ::_thesis: f . x <= f . y then consider c, d being Element of L such that A33: ( x = Class ((EqRel R),c) & y = Class ((EqRel R),d) ) and A34: k . c <= k . d by A5; ( f . x = k . c & f . y = k . d ) by A13, A33; hence f . x <= f . y by A34, YELLOW_0:60; ::_thesis: verum end; reconsider a = a as Element of L by A31; assume A35: f . x <= f . y ; ::_thesis: x <= y y in CER by A4; then consider b being set such that A36: b in the carrier of L and A37: y = Class ((EqRel R),b) by EQREL_1:def_3; reconsider b = b as Element of L by A36; A38: f . y = k . b by A13, A37; f . x = k . a by A13, A32; then k . a <= k . b by A38, A35, YELLOW_0:59; hence x <= y by A5, A32, A37; ::_thesis: verum end; then A39: f is isomorphic by A23, A30, WAYBEL_0:66; then A40: LR, Image k are_isomorphic by WAYBEL_1:def_8; then Image k,LR are_isomorphic by WAYBEL_1:6; then reconsider LR = LR as non empty strict Poset by Th15, Th16, Th17; Image k is complete by WAYBEL_1:54; then reconsider LR = LR as non empty strict complete Poset by A40, Th18, WAYBEL_1:6; reconsider LR = LR as strict complete LATTICE ; Image k is continuous LATTICE by A1, WAYBEL15:14; then reconsider LR = LR as strict complete continuous LATTICE by A40, WAYBEL15:9, WAYBEL_1:6; reconsider f9 = f " as Function of (Image k),LR by A23, A30, FUNCT_2:25; set IR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ; A41: f9 is isomorphic by A39, WAYBEL_0:68; then A42: ( corestr k is infs-preserving & f9 is infs-preserving ) by WAYBEL13:20, WAYBEL_1:56; take LR ; ::_thesis: ( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) thus the carrier of LR = Class (EqRel R) by A4; ::_thesis: ( the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) now__::_thesis:_for_z_being_set_holds_ (_(_z_in_the_InternalRel_of_LR_implies_z_in__{__[(Class_((EqRel_R),x)),(Class_((EqRel_R),y))]_where_x,_y_is_Element_of_L_:_k_._x_<=_k_._y__}__)_&_(_z_in__{__[(Class_((EqRel_R),x)),(Class_((EqRel_R),y))]_where_x,_y_is_Element_of_L_:_k_._x_<=_k_._y__}__implies_z_in_the_InternalRel_of_LR_)_) let z be set ; ::_thesis: ( ( z in the InternalRel of LR implies z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ) & ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR ) ) hereby ::_thesis: ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR ) assume A43: z in the InternalRel of LR ; ::_thesis: z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } then consider a, b being set such that A44: ( a in CER & b in CER ) and A45: z = [a,b] by A4, ZFMISC_1:def_2; reconsider a = a, b = b as Element of LR by A4, A44; a <= b by A43, A45, ORDERS_2:def_5; then ex x, y being Element of L st ( a = Class ((EqRel R),x) & b = Class ((EqRel R),y) & k . x <= k . y ) by A5; hence z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } by A45; ::_thesis: verum end; assume z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ; ::_thesis: z in the InternalRel of LR then consider x, y being Element of L such that A46: z = [(Class ((EqRel R),x)),(Class ((EqRel R),y))] and A47: k . x <= k . y ; reconsider b = Class ((EqRel R),y) as Element of LR by A4, EQREL_1:def_3; reconsider a = Class ((EqRel R),x) as Element of LR by A4, EQREL_1:def_3; a <= b by A5, A47; hence z in the InternalRel of LR by A46, ORDERS_2:def_5; ::_thesis: verum end; hence the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } by TARSKI:1; ::_thesis: for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR let g be Function of L,LR; ::_thesis: ( ( for x being Element of L holds g . x = Class ((EqRel R),x) ) implies g is CLHomomorphism of L,LR ) assume A48: for x being Element of L holds g . x = Class ((EqRel R),x) ; ::_thesis: g is CLHomomorphism of L,LR now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_ (f9_*_(corestr_k))_._x_=_g_._x let x be set ; ::_thesis: ( x in the carrier of L implies (f9 * (corestr k)) . x = g . x ) assume A49: x in the carrier of L ; ::_thesis: (f9 * (corestr k)) . x = g . x then reconsider x9 = x as Element of L ; A50: ( f . (Class ((EqRel R),x9)) = k . x9 & Class ((EqRel R),x9) in CER ) by A13, EQREL_1:def_3; dom (corestr k) = the carrier of L by FUNCT_2:def_1; hence (f9 * (corestr k)) . x = f9 . ((corestr k) . x) by A49, FUNCT_1:13 .= f9 . (k . x) by WAYBEL_1:30 .= Class ((EqRel R),x9) by A24, A23, A50, FUNCT_1:32 .= g . x by A48 ; ::_thesis: verum end; then A51: g = f9 * (corestr k) by FUNCT_2:12; A52: corestr k is directed-sups-preserving by A1, Th22; reconsider f9 = f9 as sups-preserving Function of (Image k),LR by A41, WAYBEL13:20; f9 is directed-sups-preserving ; then A53: g is directed-sups-preserving by A51, A52, WAYBEL15:11; g is infs-preserving by A51, A42, Th25; hence g is CLHomomorphism of L,LR by A53, WAYBEL16:def_1; ::_thesis: verum end; theorem Th38: :: WAYBEL20:38 for L being complete continuous LATTICE for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st ( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) holds subrelstr R is CLSubFrame of [:L,L:] proof let L be complete continuous LATTICE; ::_thesis: for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st ( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) holds subrelstr R is CLSubFrame of [:L,L:] let R be Subset of [:L,L:]; ::_thesis: ( R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st ( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ) ) implies subrelstr R is CLSubFrame of [:L,L:] ) assume R is Equivalence_Relation of the carrier of L ; ::_thesis: ( for LR being complete continuous LATTICE holds ( not the carrier of LR = Class (EqRel R) or ex g being Function of L,LR st ( ( for x being Element of L holds g . x = Class ((EqRel R),x) ) & g is not CLHomomorphism of L,LR ) ) or subrelstr R is CLSubFrame of [:L,L:] ) then A1: EqRel R = R by Def1; set ER = EqRel R; given LR being complete continuous LATTICE such that A2: the carrier of LR = Class (EqRel R) and A3: for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR ; ::_thesis: subrelstr R is CLSubFrame of [:L,L:] deffunc H1( set ) -> Element of bool the carrier of L = Class ((EqRel R),\$1); set CER = Class (EqRel R); set cL = the carrier of L; set cLR = the carrier of LR; A4: for x being set st x in the carrier of L holds H1(x) in Class (EqRel R) by EQREL_1:def_3; consider g being Function of the carrier of L,(Class (EqRel R)) such that A5: for x being set st x in the carrier of L holds g . x = H1(x) from FUNCT_2:sch_2(A4); reconsider g = g as Function of L,LR by A2; set k = g; A6: dom g = the carrier of L by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_R_implies_x_in_[:g,g:]_"_(id_the_carrier_of_LR)_)_&_(_x_in_[:g,g:]_"_(id_the_carrier_of_LR)_implies_x_in_R_)_) let x be set ; ::_thesis: ( ( x in R implies x in [:g,g:] " (id the carrier of LR) ) & ( x in [:g,g:] " (id the carrier of LR) implies x in R ) ) hereby ::_thesis: ( x in [:g,g:] " (id the carrier of LR) implies x in R ) assume A7: x in R ; ::_thesis: x in [:g,g:] " (id the carrier of LR) then x in the carrier of [:L,L:] ; then x in [: the carrier of L, the carrier of L:] by YELLOW_3:def_2; then consider x1, x2 being set such that A8: ( x1 in the carrier of L & x2 in the carrier of L ) and A9: x = [x1,x2] by ZFMISC_1:def_2; reconsider x1 = x1, x2 = x2 as Element of L by A8; A10: ( g . x1 = Class ((EqRel R),x1) & g . x2 = Class ((EqRel R),x2) ) by A5; x1 in Class ((EqRel R),x2) by A1, A7, A9, EQREL_1:19; then g . x1 = g . x2 by A10, EQREL_1:23; then A11: [(g . x1),(g . x2)] in id the carrier of LR by RELAT_1:def_10; dom [:g,g:] = [:(dom g),(dom g):] by FUNCT_3:def_8; then A12: [x1,x2] in dom [:g,g:] by A6, ZFMISC_1:87; [:g,g:] . (x1,x2) = [(g . x1),(g . x2)] by A6, FUNCT_3:def_8; hence x in [:g,g:] " (id the carrier of LR) by A9, A11, A12, FUNCT_1:def_7; ::_thesis: verum end; assume A13: x in [:g,g:] " (id the carrier of LR) ; ::_thesis: x in R then A14: [:g,g:] . x in id the carrier of LR by FUNCT_1:def_7; x in dom [:g,g:] by A13, FUNCT_1:def_7; then x in [:(dom g),(dom g):] by FUNCT_3:def_8; then consider x1, x2 being set such that A15: ( x1 in dom g & x2 in dom g ) and A16: x = [x1,x2] by ZFMISC_1:def_2; reconsider x1 = x1, x2 = x2 as Element of L by A15; A17: ( g . x1 = Class ((EqRel R),x1) & g . x2 = Class ((EqRel R),x2) ) by A5; [:g,g:] . (x1,x2) = [(g . x1),(g . x2)] by A15, FUNCT_3:def_8; then g . x1 = g . x2 by A14, A16, RELAT_1:def_10; then x1 in Class ((EqRel R),x2) by A17, EQREL_1:23; hence x in R by A1, A16, EQREL_1:19; ::_thesis: verum end; then A18: R = [:g,g:] " (id the carrier of LR) by TARSKI:1; for x being Element of L holds g . x = Class ((EqRel R),x) by A5; then g is CLHomomorphism of L,LR by A3; hence subrelstr R is CLSubFrame of [:L,L:] by A18, Th34; ::_thesis: verum end; registration let L be non empty reflexive RelStr ; cluster non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of L) directed-sups-preserving kernel for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Function of L,L st ( b1 is directed-sups-preserving & b1 is kernel ) proof reconsider k = id L as directed-sups-preserving kernel Function of L,L ; take k ; ::_thesis: ( k is directed-sups-preserving & k is kernel ) thus ( k is directed-sups-preserving & k is kernel ) ; ::_thesis: verum end; end; definition let L be non empty reflexive RelStr ; let k be kernel Function of L,L; func kernel_congruence k -> non empty Subset of [:L,L:] equals :: WAYBEL20:def 4 [:k,k:] " (id the carrier of L); coherence [:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:] proof set cL = the carrier of L; set x = the Element of the carrier of L; A1: dom k = the carrier of L by FUNCT_2:def_1; then A2: ( [(k . the Element of the carrier of L),(k . the Element of the carrier of L)] in id the carrier of L & [:k,k:] . ( the Element of the carrier of L, the Element of the carrier of L) = [(k . the Element of the carrier of L),(k . the Element of the carrier of L)] ) by FUNCT_3:def_8, RELAT_1:def_10; dom [:k,k:] = [:(dom k),(dom k):] by FUNCT_3:def_8; then [ the Element of the carrier of L, the Element of the carrier of L] in dom [:k,k:] by A1, ZFMISC_1:def_2; hence [:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:] by A2, FUNCT_1:def_7; ::_thesis: verum end; end; :: deftheorem defines kernel_congruence WAYBEL20:def_4_:_ for L being non empty reflexive RelStr for k being kernel Function of L,L holds kernel_congruence k = [:k,k:] " (id the carrier of L); theorem :: WAYBEL20:39 for L being non empty reflexive RelStr for k being kernel Function of L,L holds kernel_congruence k is Equivalence_Relation of the carrier of L by Th2; theorem Th40: :: WAYBEL20:40 for L being complete continuous LATTICE for k being directed-sups-preserving kernel Function of L,L holds kernel_congruence k is CLCongruence proof let L be complete continuous LATTICE; ::_thesis: for k being directed-sups-preserving kernel Function of L,L holds kernel_congruence k is CLCongruence let k be directed-sups-preserving kernel Function of L,L; ::_thesis: kernel_congruence k is CLCongruence set R = kernel_congruence k; thus A1: kernel_congruence k is Equivalence_Relation of the carrier of L by Th2; :: according to WAYBEL20:def_2 ::_thesis: subrelstr (kernel_congruence k) is CLSubFrame of [:L,L:] ex LR being strict complete continuous LATTICE st ( the carrier of LR = Class (EqRel (kernel_congruence k)) & the InternalRel of LR = { [(Class ((EqRel (kernel_congruence k)),x)),(Class ((EqRel (kernel_congruence k)),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel (kernel_congruence k)),x) ) holds g is CLHomomorphism of L,LR ) ) by Th37; hence subrelstr (kernel_congruence k) is CLSubFrame of [:L,L:] by A1, Th38; ::_thesis: verum end; definition let L be complete continuous LATTICE; let R be non empty Subset of [:L,L:]; assume B1: R is CLCongruence ; funcL ./. R -> strict complete continuous LATTICE means :Def5: :: WAYBEL20:def 5 ( the carrier of it = Class (EqRel R) & ( for x, y being Element of it holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ); existence ex b1 being strict complete continuous LATTICE st ( the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) proof set k = kernel_op R; ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) by B1, Th36; then consider LR being strict complete continuous LATTICE such that A1: the carrier of LR = Class (EqRel R) and A2: the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : (kernel_op R) . x <= (kernel_op R) . y } and for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds g is CLHomomorphism of L,LR by Th37; take LR ; ::_thesis: ( the carrier of LR = Class (EqRel R) & ( for x, y being Element of LR holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) thus the carrier of LR = Class (EqRel R) by A1; ::_thesis: for x, y being Element of LR holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) let x, y be Element of LR; ::_thesis: ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) x in the carrier of LR ; then consider u being set such that A3: u in the carrier of L and A4: x = Class ((EqRel R),u) by A1, EQREL_1:def_3; y in the carrier of LR ; then consider v being set such that A5: v in the carrier of L and A6: y = Class ((EqRel R),v) by A1, EQREL_1:def_3; hereby ::_thesis: ( "/\" (x,L) <= "/\" (y,L) implies x <= y ) assume x <= y ; ::_thesis: "/\" (x,L) <= "/\" (y,L) then [x,y] in the InternalRel of LR by ORDERS_2:def_5; then consider u9, v9 being Element of L such that A7: [x,y] = [(Class ((EqRel R),u9)),(Class ((EqRel R),v9))] and A8: (kernel_op R) . u9 <= (kernel_op R) . v9 by A2; A9: ( x = Class ((EqRel R),u9) & y = Class ((EqRel R),v9) ) by A7, XTUPLE_0:1; (kernel_op R) . u9 = inf (Class ((EqRel R),u9)) by B1, Def3; hence "/\" (x,L) <= "/\" (y,L) by B1, A8, A9, Def3; ::_thesis: verum end; assume A10: "/\" (x,L) <= "/\" (y,L) ; ::_thesis: x <= y reconsider u = u, v = v as Element of L by A3, A5; ( (kernel_op R) . u = inf (Class ((EqRel R),u)) & (kernel_op R) . v = inf (Class ((EqRel R),v)) ) by B1, Def3; then [x,y] in the InternalRel of LR by A2, A4, A6, A10; hence x <= y by ORDERS_2:def_5; ::_thesis: verum end; uniqueness for b1, b2 being strict complete continuous LATTICE st the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of b2 = Class (EqRel R) & ( for x, y being Element of b2 holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) holds b1 = b2 proof let LR1, LR2 be strict complete continuous LATTICE; ::_thesis: ( the carrier of LR1 = Class (EqRel R) & ( for x, y being Element of LR1 holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of LR2 = Class (EqRel R) & ( for x, y being Element of LR2 holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) implies LR1 = LR2 ) assume that A11: the carrier of LR1 = Class (EqRel R) and A12: for x, y being Element of LR1 holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) and A13: the carrier of LR2 = Class (EqRel R) and A14: for x, y being Element of LR2 holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ; ::_thesis: LR1 = LR2 set cLR2 = the carrier of LR2; set cLR1 = the carrier of LR1; now__::_thesis:_for_z_being_set_holds_ (_(_z_in_the_InternalRel_of_LR1_implies_z_in_the_InternalRel_of_LR2_)_&_(_z_in_the_InternalRel_of_LR2_implies_z_in_the_InternalRel_of_LR1_)_) let z be set ; ::_thesis: ( ( z in the InternalRel of LR1 implies z in the InternalRel of LR2 ) & ( z in the InternalRel of LR2 implies z in the InternalRel of LR1 ) ) hereby ::_thesis: ( z in the InternalRel of LR2 implies z in the InternalRel of LR1 ) assume A15: z in the InternalRel of LR1 ; ::_thesis: z in the InternalRel of LR2 then consider x, y being set such that A16: ( x in the carrier of LR1 & y in the carrier of LR1 ) and A17: z = [x,y] by ZFMISC_1:def_2; reconsider x = x, y = y as Element of LR1 by A16; reconsider x9 = x, y9 = y as Element of LR2 by A11, A13; x <= y by A15, A17, ORDERS_2:def_5; then "/\" (x,L) <= "/\" (y,L) by A12; then x9 <= y9 by A14; hence z in the InternalRel of LR2 by A17, ORDERS_2:def_5; ::_thesis: verum end; assume A18: z in the InternalRel of LR2 ; ::_thesis: z in the InternalRel of LR1 then consider x, y being set such that A19: ( x in the carrier of LR2 & y in the carrier of LR2 ) and A20: z = [x,y] by ZFMISC_1:def_2; reconsider x = x, y = y as Element of LR2 by A19; reconsider x9 = x, y9 = y as Element of LR1 by A11, A13; x <= y by A18, A20, ORDERS_2:def_5; then "/\" (x,L) <= "/\" (y,L) by A14; then x9 <= y9 by A12; hence z in the InternalRel of LR1 by A20, ORDERS_2:def_5; ::_thesis: verum end; hence LR1 = LR2 by A11, A13, TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def5 defines ./. WAYBEL20:def_5_:_ for L being complete continuous LATTICE for R being non empty Subset of [:L,L:] st R is CLCongruence holds for b3 being strict complete continuous LATTICE holds ( b3 = L ./. R iff ( the carrier of b3 = Class (EqRel R) & ( for x, y being Element of b3 holds ( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) ); theorem :: WAYBEL20:41 for L being complete continuous LATTICE for R being non empty Subset of [:L,L:] st R is CLCongruence holds for x being set holds ( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) ) proof let L be complete continuous LATTICE; ::_thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds for x being set holds ( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) ) let R be non empty Subset of [:L,L:]; ::_thesis: ( R is CLCongruence implies for x being set holds ( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) ) ) assume R is CLCongruence ; ::_thesis: for x being set holds ( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) ) then A1: the carrier of (L ./. R) = Class (EqRel R) by Def5; let x be set ; ::_thesis: ( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) ) hereby ::_thesis: ( ex y being Element of L st x = Class ((EqRel R),y) implies x is Element of (L ./. R) ) assume x is Element of (L ./. R) ; ::_thesis: ex y being Element of L st x = Class ((EqRel R),y) then x in Class (EqRel R) by A1; then consider y being set such that A2: y in the carrier of L and A3: x = Class ((EqRel R),y) by EQREL_1:def_3; reconsider y = y as Element of L by A2; take y = y; ::_thesis: x = Class ((EqRel R),y) thus x = Class ((EqRel R),y) by A3; ::_thesis: verum end; given y being Element of L such that A4: x = Class ((EqRel R),y) ; ::_thesis: x is Element of (L ./. R) thus x is Element of (L ./. R) by A1, A4, EQREL_1:def_3; ::_thesis: verum end; theorem :: WAYBEL20:42 for L being complete continuous LATTICE for R being non empty Subset of [:L,L:] st R is CLCongruence holds R = kernel_congruence (kernel_op R) by Th36; theorem :: WAYBEL20:43 for L being complete continuous LATTICE for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k) proof let L be complete continuous LATTICE; ::_thesis: for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k) let k be directed-sups-preserving kernel Function of L,L; ::_thesis: k = kernel_op (kernel_congruence k) set kc = kernel_congruence k; set cL = the carrier of L; set km = kernel_op (kernel_congruence k); A1: dom k = the carrier of L by FUNCT_2:def_1; A2: kernel_op (kernel_congruence k) <= id L by WAYBEL_1:def_15; A3: k <= id L by WAYBEL_1:def_15; A4: kernel_congruence k is CLCongruence by Th40; then A5: kernel_congruence k = [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] " (id the carrier of L) by Th36; reconsider kc9 = kernel_congruence k as Equivalence_Relation of the carrier of L by A4, Def2; field kc9 = the carrier of L by ORDERS_1:12; then A6: kc9 is_transitive_in the carrier of L by RELAT_2:def_16; A7: dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] = [:(dom (kernel_op (kernel_congruence k))),(dom (kernel_op (kernel_congruence k))):] by FUNCT_3:def_8; A8: dom (kernel_op (kernel_congruence k)) = the carrier of L by FUNCT_2:def_1; A9: dom [:k,k:] = [:(dom k),(dom k):] by FUNCT_3:def_8; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_ k_._x_=_(kernel_op_(kernel_congruence_k))_._x let x be set ; ::_thesis: ( x in the carrier of L implies k . x = (kernel_op (kernel_congruence k)) . x ) assume x in the carrier of L ; ::_thesis: k . x = (kernel_op (kernel_congruence k)) . x then reconsider x9 = x as Element of L ; A10: k . (k . x9) = (k * k) . x9 by A1, FUNCT_1:13 .= k . x9 by QUANTAL1:def_9 ; A11: ( [(k . x9),(k . x9)] in id the carrier of L & [:k,k:] . ((k . x9),x9) = [(k . (k . x9)),(k . x9)] ) by A1, FUNCT_3:def_8, RELAT_1:def_10; [(k . x9),x9] in dom [:k,k:] by A1, A9, ZFMISC_1:def_2; then A12: [(k . x9),x9] in kernel_congruence k by A10, A11, FUNCT_1:def_7; A13: (kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9) = ((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x9 by A8, FUNCT_1:13 .= (kernel_op (kernel_congruence k)) . x9 by QUANTAL1:def_9 ; (kernel_op (kernel_congruence k)) . (k . x9) <= (id L) . (k . x9) by A2, YELLOW_2:9; then A14: (kernel_op (kernel_congruence k)) . (k . x9) <= k . x9 by FUNCT_1:18; A15: ( [((kernel_op (kernel_congruence k)) . x9),((kernel_op (kernel_congruence k)) . x9)] in id the carrier of L & [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . (x9,((kernel_op (kernel_congruence k)) . x9)) = [((kernel_op (kernel_congruence k)) . x9),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9))] ) by A8, FUNCT_3:def_8, RELAT_1:def_10; [x9,((kernel_op (kernel_congruence k)) . x9)] in dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] by A8, A7, ZFMISC_1:def_2; then [x9,((kernel_op (kernel_congruence k)) . x9)] in kernel_congruence k by A5, A13, A15, FUNCT_1:def_7; then A16: [(k . x9),((kernel_op (kernel_congruence k)) . x9)] in kernel_congruence k by A6, A12, RELAT_2:def_8; then [:k,k:] . ((k . x9),((kernel_op (kernel_congruence k)) . x9)) in id the carrier of L by FUNCT_1:def_7; then [(k . (k . x9)),(k . ((kernel_op (kernel_congruence k)) . x9))] in id the carrier of L by A1, FUNCT_3:def_8; then A17: k . ((kernel_op (kernel_congruence k)) . x9) = k . (k . x9) by RELAT_1:def_10 .= (k * k) . x9 by A1, FUNCT_1:13 .= k . x9 by QUANTAL1:def_9 ; [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . ((k . x9),((kernel_op (kernel_congruence k)) . x9)) in id the carrier of L by A5, A16, FUNCT_1:def_7; then [((kernel_op (kernel_congruence k)) . (k . x9)),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9))] in id the carrier of L by A8, FUNCT_3:def_8; then A18: (kernel_op (kernel_congruence k)) . (k . x9) = (kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9) by RELAT_1:def_10 .= ((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x9 by A8, FUNCT_1:13 .= (kernel_op (kernel_congruence k)) . x9 by QUANTAL1:def_9 ; k . ((kernel_op (kernel_congruence k)) . x9) <= (id L) . ((kernel_op (kernel_congruence k)) . x9) by A3, YELLOW_2:9; then k . ((kernel_op (kernel_congruence k)) . x9) <= (kernel_op (kernel_congruence k)) . x9 by FUNCT_1:18; hence k . x = (kernel_op (kernel_congruence k)) . x by A17, A18, A14, YELLOW_0:def_3; ::_thesis: verum end; hence k = kernel_op (kernel_congruence k) by FUNCT_2:12; ::_thesis: verum end; theorem :: WAYBEL20:44 for L being complete continuous LATTICE for p being projection Function of L,L st p is infs-preserving holds ( Image p is continuous LATTICE & Image p is infs-inheriting ) proof let L be complete continuous LATTICE; ::_thesis: for p being projection Function of L,L st p is infs-preserving holds ( Image p is continuous LATTICE & Image p is infs-inheriting ) let p be projection Function of L,L; ::_thesis: ( p is infs-preserving implies ( Image p is continuous LATTICE & Image p is infs-inheriting ) ) assume A1: p is infs-preserving ; ::_thesis: ( Image p is continuous LATTICE & Image p is infs-inheriting ) reconsider Lc = { c where c is Element of L : c <= p . c } as non empty Subset of L by WAYBEL_1:43; reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by WAYBEL_1:45; A2: subrelstr Lc is infs-inheriting by A1, WAYBEL_1:51; then A3: subrelstr Lc is complete by YELLOW_2:30; A4: pc is infs-preserving proof let X be Subset of (subrelstr Lc); :: according to WAYBEL_0:def_32 ::_thesis: pc preserves_inf_of X assume ex_inf_of X, subrelstr Lc ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of pc .: X, subrelstr Lc & "/\" ((pc .: X),(subrelstr Lc)) = pc . ("/\" (X,(subrelstr Lc))) ) thus ex_inf_of pc .: X, subrelstr Lc by A3, YELLOW_0:17; ::_thesis: "/\" ((pc .: X),(subrelstr Lc)) = pc . ("/\" (X,(subrelstr Lc))) the carrier of (subrelstr Lc) = Lc by YELLOW_0:def_15; then reconsider X9 = X as Subset of L by XBOOLE_1:1; A5: ( ex_inf_of X9,L & p preserves_inf_of X9 ) by A1, WAYBEL_0:def_32, YELLOW_0:17; X c= the carrier of (subrelstr Lc) ; then X c= Lc by YELLOW_0:def_15; then A6: pc .: X = p .: X by RELAT_1:129; A7: ex_inf_of X,L by YELLOW_0:17; then "/\" (X9,L) in the carrier of (subrelstr Lc) by A2, YELLOW_0:def_18; then A8: ( dom pc = the carrier of (subrelstr Lc) & inf X9 = inf X ) by A7, FUNCT_2:def_1, YELLOW_0:63; ( ex_inf_of p .: X,L & "/\" ((pc .: X),L) in the carrier of (subrelstr Lc) ) by A2, YELLOW_0:17, YELLOW_0:def_18; hence inf (pc .: X) = inf (p .: X) by A6, YELLOW_0:63 .= p . (inf X9) by A5, WAYBEL_0:def_30 .= pc . (inf X) by A8, FUNCT_1:47 ; ::_thesis: verum end; reconsider cpc = corestr pc as Function of (subrelstr Lc),(Image pc) ; A9: the carrier of (subrelstr (rng p)) = rng p by YELLOW_0:def_15 .= rng pc by WAYBEL_1:44 .= the carrier of (subrelstr (rng pc)) by YELLOW_0:def_15 ; subrelstr (rng pc) is full SubRelStr of L by WAYBEL15:1; then A10: Image p = Image pc by A9, YELLOW_0:57; pc is closure by WAYBEL_1:47; then A11: cpc is sups-preserving by WAYBEL_1:55; subrelstr Lc is sups-inheriting SubRelStr of L by WAYBEL_1:49; then subrelstr Lc is continuous LATTICE by A2, WAYBEL_5:28; hence Image p is continuous LATTICE by A3, A10, A4, A11, Th19, WAYBEL_5:33; ::_thesis: Image p is infs-inheriting thus Image p is infs-inheriting by A1, A2, WAYBEL_1:51; ::_thesis: verum end;