:: WAYBEL34 semantic presentation

begin

registration
let S, T be complete LATTICE;
cluster Galois for Connection of S,T;
existence
 ex b1 being Connection of S,T st b1 is Galois
proof
set g = the infs-preserving Function of S,T;
 the infs-preserving Function of S,T is upper_adjoint by WAYBEL_1:16;
then  ex d being Function of T,S st [ the infs-preserving Function of S,T,d] is Galois by WAYBEL_1:def_11;
hence  ex b1 being Connection of S,T st b1 is Galois ; ::_thesis: verum
end;
end;

theorem Th1: :: WAYBEL34:1
for S, T, S9, T9 being non empty RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds
for c being Connection of S,T
for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois
proof
let S, T, S9, T9 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) implies for c being Connection of S,T
for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois )
assume that
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) and
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) ; ::_thesis: for c being Connection of S,T
for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois
let c be Connection of S,T; ::_thesis: for c9 being Connection of S9,T9 st c = c9 & c is Galois holds
c9 is Galois
let c9 be Connection of S9,T9; ::_thesis: ( c = c9 & c is Galois implies c9 is Galois )
assume A3: c = c9 ; ::_thesis: ( not c is Galois or c9 is Galois )
given g being Function of S,T, d being Function of T,S such that A4: c = [g,d] and
A5: g is monotone and
A6: d is monotone and
A7: for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ; :: according to WAYBEL_1:def_10 ::_thesis: c9 is Galois
reconsider g9 = g as Function of S9,T9 by A1, A2;
reconsider d9 = d as Function of T9,S9 by A1, A2;
take  g9 ; :: according to WAYBEL_1:def_10 ::_thesis: ex b1 being Element of bool [: the carrier of T9, the carrier of S9:] st
( c9 = [g9,b1] & g9 is monotone & b1 is monotone & ( for b2 being Element of the carrier of T9
for b3 being Element of the carrier of S9 holds
( ( not b2 <= g9 . b3 or b1 . b2 <= b3 ) & ( not b1 . b2 <= b3 or b2 <= g9 . b3 ) ) ) )
take  d9 ; ::_thesis: ( c9 = [g9,d9] & g9 is monotone & d9 is monotone & ( for b1 being Element of the carrier of T9
for b2 being Element of the carrier of S9 holds
( ( not b1 <= g9 . b2 or d9 . b1 <= b2 ) & ( not d9 . b1 <= b2 or b1 <= g9 . b2 ) ) ) )
thus  c9 = [g9,d9] by A3, A4; ::_thesis: ( g9 is monotone & d9 is monotone & ( for b1 being Element of the carrier of T9
for b2 being Element of the carrier of S9 holds
( ( not b1 <= g9 . b2 or d9 . b1 <= b2 ) & ( not d9 . b1 <= b2 or b1 <= g9 . b2 ) ) ) )
thus  ( g9 is monotone & d9 is monotone ) by A1, A2, A5, A6, WAYBEL_9:1; ::_thesis: for b1 being Element of the carrier of T9
for b2 being Element of the carrier of S9 holds
( ( not b1 <= g9 . b2 or d9 . b1 <= b2 ) & ( not d9 . b1 <= b2 or b1 <= g9 . b2 ) )
let t9 be Element of T9; ::_thesis: for b1 being Element of the carrier of S9 holds
( ( not t9 <= g9 . b1 or d9 . t9 <= b1 ) & ( not d9 . t9 <= b1 or t9 <= g9 . b1 ) )
let s9 be Element of S9; ::_thesis: ( ( not t9 <= g9 . s9 or d9 . t9 <= s9 ) & ( not d9 . t9 <= s9 or t9 <= g9 . s9 ) )
reconsider t = t9 as Element of T by A2;
reconsider s = s9 as Element of S by A1;
A8: ( t9 <= g9 . s9 iff t <= g . s ) by A2, YELLOW_0:1;
 ( d9 . t9 <= s9 iff d . t <= s ) by A1, YELLOW_0:1;
hence  ( ( not t9 <= g9 . s9 or d9 . t9 <= s9 ) & ( not d9 . t9 <= s9 or t9 <= g9 . s9 ) ) by A7, A8; ::_thesis: verum
end;

definition
let S, T be LATTICE;
let g be Function of S,T;
assume that
A1: S is complete and
A2: g is infs-preserving ;
A3: g is upper_adjoint by A1, A2, WAYBEL_1:16;
func LowerAdj g ->  Function of T,S means :Def1: :: WAYBEL34:def 1
[g,it] is Galois ;
uniqueness
 for b1, b2 being Function of T,S st [g,b1] is Galois & [g,b2] is Galois holds
b1 = b2
proof
let d1, d2 be Function of T,S; ::_thesis: ( [g,d1] is Galois & [g,d2] is Galois implies d1 = d2 )
assume that
A4: [g,d1] is Galois and
A5: [g,d2] is Galois ; ::_thesis: d1 = d2
now__::_thesis:_for_t_being_Element_of_T_holds_d1_._t_=_d2_._t
let t be Element of T; ::_thesis: d1 . t = d2 . t
reconsider t9 = t as Element of T ;
A6: d1 . t9 is_minimum_of g " (uparrow t) by A4, WAYBEL_1:10;
A7: d2 . t9 is_minimum_of g " (uparrow t) by A5, WAYBEL_1:10;
 d1 . t = "/\" ((g " (uparrow t)),S) by A6, WAYBEL_1:def_6;
hence  d1 . t = d2 . t by A7, WAYBEL_1:def_6; ::_thesis: verum
end;
hence  d1 = d2 by FUNCT_2:63; ::_thesis: verum
end;
existence
 ex b1 being Function of T,S st [g,b1] is Galois by A3, WAYBEL_1:def_11;
end;

:: deftheorem Def1 defines LowerAdj WAYBEL34:def_1_:_
 for S, T being LATTICE
for g being Function of S,T st S is complete & g is infs-preserving holds
for b4 being Function of T,S holds
( b4 = LowerAdj g iff [g,b4] is Galois );

definition
let S, T be LATTICE;
let d be Function of T,S;
assume that
A1: T is complete and
A2: d is sups-preserving ;
A3: d is lower_adjoint by A1, A2, WAYBEL_1:17;
func UpperAdj d ->  Function of S,T means :Def2: :: WAYBEL34:def 2
[it,d] is Galois ;
existence
 ex b1 being Function of S,T st [b1,d] is Galois by A3, WAYBEL_1:def_12;
correctness
uniqueness
for b1, b2 being Function of S,T st [b1,d] is Galois & [b2,d] is Galois holds
b1 = b2;
proof
let g1, g2 be Function of S,T; ::_thesis: ( [g1,d] is Galois & [g2,d] is Galois implies g1 = g2 )
assume that
A4: [g1,d] is Galois and
A5: [g2,d] is Galois ; ::_thesis: g1 = g2
now__::_thesis:_for_t_being_Element_of_S_holds_g1_._t_=_g2_._t
let t be Element of S; ::_thesis: g1 . t = g2 . t
reconsider t9 = t as Element of S ;
A6: g1 . t9 is_maximum_of d " (downarrow t) by A4, WAYBEL_1:11;
A7: g2 . t9 is_maximum_of d " (downarrow t) by A5, WAYBEL_1:11;
 g1 . t = "\/" ((d " (downarrow t)),T) by A6, WAYBEL_1:def_7;
hence  g1 . t = g2 . t by A7, WAYBEL_1:def_7; ::_thesis: verum
end;
hence  g1 = g2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines UpperAdj WAYBEL34:def_2_:_
 for S, T being LATTICE
for d being Function of T,S st T is complete & d is sups-preserving holds
for b4 being Function of S,T holds
( b4 = UpperAdj d iff [b4,d] is Galois );

Lm1: now__::_thesis:_for_S,_T_being_LATTICE_st_S_is_complete_&_T_is_complete_holds_
for_g_being_Function_of_S,T_st_g_is_infs-preserving_holds_
(_LowerAdj_g_is_monotone_&_LowerAdj_g_is_lower_adjoint_&_LowerAdj_g_is_sups-preserving_)
let S, T be LATTICE; ::_thesis: ( S is complete & T is complete implies for g being Function of S,T st g is infs-preserving holds
( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) )
assume that
A1: S is complete and
A2: T is complete ; ::_thesis: for g being Function of S,T st g is infs-preserving holds
( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving )
reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;
let g be Function of S,T; ::_thesis: ( g is infs-preserving implies ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) )
assume  g is infs-preserving ; ::_thesis: ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving )
then reconsider g9 = g as infs-preserving Function of S9,T9 ;
 [g9,(LowerAdj g9)] is Galois by Def1;
then  ( LowerAdj g9 is lower_adjoint & LowerAdj g9 is monotone ) by WAYBEL_1:8, WAYBEL_1:def_12;
hence  ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) ; ::_thesis: verum
end;

Lm2: now__::_thesis:_for_S,_T_being_LATTICE_st_S_is_complete_&_T_is_complete_holds_
for_g_being_Function_of_S,T_st_g_is_sups-preserving_holds_
(_UpperAdj_g_is_monotone_&_UpperAdj_g_is_upper_adjoint_&_UpperAdj_g_is_infs-preserving_)
let S, T be LATTICE; ::_thesis: ( S is complete & T is complete implies for g being Function of S,T st g is sups-preserving holds
( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) )
assume that
A1: S is complete and
A2: T is complete ; ::_thesis: for g being Function of S,T st g is sups-preserving holds
( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving )
reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;
let g be Function of S,T; ::_thesis: ( g is sups-preserving implies ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) )
assume  g is sups-preserving ; ::_thesis: ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving )
then reconsider g9 = g as sups-preserving Function of S9,T9 ;
 [(UpperAdj g9),g9] is Galois by Def2;
then  ( UpperAdj g9 is upper_adjoint & UpperAdj g9 is monotone ) by WAYBEL_1:8, WAYBEL_1:def_11;
hence  ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) ; ::_thesis: verum
end;

registration
let S, T be complete LATTICE;
let g be infs-preserving Function of S,T;
cluster LowerAdj g ->  lower_adjoint ;
coherence
 LowerAdj g is lower_adjoint by Lm1;
end;

registration
let S, T be complete LATTICE;
let d be sups-preserving Function of T,S;
cluster UpperAdj d ->  upper_adjoint ;
coherence
 UpperAdj d is upper_adjoint by Lm2;
end;

theorem :: WAYBEL34:2
for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for t being Element of T holds (LowerAdj g) . t = inf (g " (uparrow t))
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T
for t being Element of T holds (LowerAdj g) . t = inf (g " (uparrow t))
let g be infs-preserving Function of S,T; ::_thesis: for t being Element of T holds (LowerAdj g) . t = inf (g " (uparrow t))
let t be Element of T; ::_thesis: (LowerAdj g) . t = inf (g " (uparrow t))
 [g,(LowerAdj g)] is Galois by Def1;
then  (LowerAdj g) . t is_minimum_of g " (uparrow t) by WAYBEL_1:10;
hence  (LowerAdj g) . t = inf (g " (uparrow t)) by WAYBEL_1:def_6; ::_thesis: verum
end;

theorem :: WAYBEL34:3
for S, T being complete LATTICE
for d being sups-preserving Function of T,S
for s being Element of S holds (UpperAdj d) . s = sup (d " (downarrow s))
proof
let S, T be complete LATTICE; ::_thesis: for d being sups-preserving Function of T,S
for s being Element of S holds (UpperAdj d) . s = sup (d " (downarrow s))
let d be sups-preserving Function of T,S; ::_thesis: for s being Element of S holds (UpperAdj d) . s = sup (d " (downarrow s))
let s be Element of S; ::_thesis: (UpperAdj d) . s = sup (d " (downarrow s))
 [(UpperAdj d),d] is Galois by Def2;
then  (UpperAdj d) . s is_maximum_of d " (downarrow s) by WAYBEL_1:11;
hence  (UpperAdj d) . s = sup (d " (downarrow s)) by WAYBEL_1:def_7; ::_thesis: verum
end;

definition
let S, T be RelStr ;
let f be Function of the carrier of S, the carrier of T;
funcf opp  ->  Function of (S opp),(T opp) equals :: WAYBEL34:def 3
f;
coherence
 f is Function of (S opp),(T opp) ;
end;

:: deftheorem  defines opp WAYBEL34:def_3_:_
 for S, T being RelStr
for f being Function of the carrier of S, the carrier of T holds f opp = f;

registration
let S, T be complete LATTICE;
let g be infs-preserving Function of S,T;
clusterg opp  ->  lower_adjoint ;
coherence
 g opp is lower_adjoint
proof
 [g,(LowerAdj g)] is Galois by Def1;
then  [((LowerAdj g) opp),(g opp)] is Galois by YELLOW_7:44;
hence  g opp is lower_adjoint by WAYBEL_1:def_12; ::_thesis: verum
end;
end;

registration
let S, T be complete LATTICE;
let d be sups-preserving Function of S,T;
clusterd opp  ->  upper_adjoint ;
coherence
 d opp is upper_adjoint
proof
 [(UpperAdj d),d] is Galois by Def2;
then  [(d opp),((UpperAdj d) opp)] is Galois by YELLOW_7:44;
hence  d opp is upper_adjoint by WAYBEL_1:def_11; ::_thesis: verum
end;
end;

theorem :: WAYBEL34:4
for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds LowerAdj g = UpperAdj (g opp)
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T holds LowerAdj g = UpperAdj (g opp)
let g be infs-preserving Function of S,T; ::_thesis: LowerAdj g = UpperAdj (g opp)
 [g,(LowerAdj g)] is Galois by Def1;
then  [((LowerAdj g) opp),(g opp)] is Galois by YELLOW_7:44;
hence  LowerAdj g = UpperAdj (g opp) by Def2; ::_thesis: verum
end;

theorem :: WAYBEL34:5
for S, T being complete LATTICE
for d being sups-preserving Function of S,T holds LowerAdj (d opp) = UpperAdj d
proof
let S, T be complete LATTICE; ::_thesis: for d being sups-preserving Function of S,T holds LowerAdj (d opp) = UpperAdj d
let d be sups-preserving Function of S,T; ::_thesis: LowerAdj (d opp) = UpperAdj d
 [(UpperAdj d),d] is Galois by Def2;
then  [(d opp),((UpperAdj d) opp)] is Galois by YELLOW_7:44;
hence  LowerAdj (d opp) = UpperAdj d by Def1; ::_thesis: verum
end;

theorem Th6: :: WAYBEL34:6
for L being non empty RelStr holds [(id L),(id L)] is Galois
proof
let L be non empty RelStr ; ::_thesis: [(id L),(id L)] is Galois
take g = id L; :: according to WAYBEL_1:def_10 ::_thesis: ex b1 being Element of bool [: the carrier of L, the carrier of L:] st
( [(id L),(id L)] = [g,b1] & g is monotone & b1 is monotone & ( for b2, b3 being Element of the carrier of L holds
( ( not b2 <= g . b3 or b1 . b2 <= b3 ) & ( not b1 . b2 <= b3 or b2 <= g . b3 ) ) ) )
take d = id L; ::_thesis: ( [(id L),(id L)] = [g,d] & g is monotone & d is monotone & ( for b1, b2 being Element of the carrier of L holds
( ( not b1 <= g . b2 or d . b1 <= b2 ) & ( not d . b1 <= b2 or b1 <= g . b2 ) ) ) )
thus  ( [(id L),(id L)] = [g,d] & g is monotone & d is monotone ) ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( ( not b1 <= g . b2 or d . b1 <= b2 ) & ( not d . b1 <= b2 or b1 <= g . b2 ) )
let t, s be Element of L; ::_thesis: ( ( not t <= g . s or d . t <= s ) & ( not d . t <= s or t <= g . s ) )
 g . s = s by FUNCT_1:18;
hence  ( ( not t <= g . s or d . t <= s ) & ( not d . t <= s or t <= g . s ) ) by FUNCT_1:18; ::_thesis: verum
end;

theorem Th7: :: WAYBEL34:7
for L being complete LATTICE holds
( LowerAdj (id L) = id L & UpperAdj (id L) = id L )
proof
let L be complete LATTICE; ::_thesis: ( LowerAdj (id L) = id L & UpperAdj (id L) = id L )
 [(id L),(id L)] is Galois by Th6;
hence  ( LowerAdj (id L) = id L & UpperAdj (id L) = id L ) by Def1, Def2; ::_thesis: verum
end;

theorem Th8: :: WAYBEL34:8
for L1, L2, L3 being complete LATTICE
for g1 being infs-preserving Function of L1,L2
for g2 being infs-preserving Function of L2,L3 holds LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2)
proof
let L1, L2, L3 be complete LATTICE; ::_thesis: for g1 being infs-preserving Function of L1,L2
for g2 being infs-preserving Function of L2,L3 holds LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2)
let g1 be infs-preserving Function of L1,L2; ::_thesis: for g2 being infs-preserving Function of L2,L3 holds LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2)
let g2 be infs-preserving Function of L2,L3; ::_thesis: LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2)
A1: [g1,(LowerAdj g1)] is Galois by Def1;
 [g2,(LowerAdj g2)] is Galois by Def1;
then A2: [(g2 * g1),((LowerAdj g1) * (LowerAdj g2))] is Galois by A1, WAYBEL15:5;
 g2 * g1 is infs-preserving by WAYBEL20:25;
hence  LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2) by A2, Def1; ::_thesis: verum
end;

theorem Th9: :: WAYBEL34:9
for L1, L2, L3 being complete LATTICE
for d1 being sups-preserving Function of L1,L2
for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
proof
let L1, L2, L3 be complete LATTICE; ::_thesis: for d1 being sups-preserving Function of L1,L2
for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
let d1 be sups-preserving Function of L1,L2; ::_thesis: for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
let d2 be sups-preserving Function of L2,L3; ::_thesis: UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
A1: [(UpperAdj d1),d1] is Galois by Def2;
 [(UpperAdj d2),d2] is Galois by Def2;
then A2: [((UpperAdj d1) * (UpperAdj d2)),(d2 * d1)] is Galois by A1, WAYBEL15:5;
 d2 * d1 is sups-preserving by WAYBEL20:27;
hence  UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2) by A2, Def2; ::_thesis: verum
end;

theorem Th10: :: WAYBEL34:10
for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds UpperAdj (LowerAdj g) = g
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T holds UpperAdj (LowerAdj g) = g
let g be infs-preserving Function of S,T; ::_thesis: UpperAdj (LowerAdj g) = g
 [g,(LowerAdj g)] is Galois by Def1;
hence  UpperAdj (LowerAdj g) = g by Def2; ::_thesis: verum
end;

theorem Th11: :: WAYBEL34:11
for S, T being complete LATTICE
for d being sups-preserving Function of S,T holds LowerAdj (UpperAdj d) = d
proof
let S, T be complete LATTICE; ::_thesis: for d being sups-preserving Function of S,T holds LowerAdj (UpperAdj d) = d
let d be sups-preserving Function of S,T; ::_thesis: LowerAdj (UpperAdj d) = d
 [(UpperAdj d),d] is Galois by Def2;
hence  LowerAdj (UpperAdj d) = d by Def1; ::_thesis: verum
end;

theorem Th12: :: WAYBEL34:12
for C being non empty AltCatStr
for a, b, f being set st f in the Arrows of C . (a,b) holds
ex o1, o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
proof
let C be non empty AltCatStr ; ::_thesis: for a, b, f being set st f in the Arrows of C . (a,b) holds
ex o1, o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
let a, b, f be set ; ::_thesis: ( f in the Arrows of C . (a,b) implies ex o1, o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 ) )
assume A1: f in the Arrows of C . (a,b) ; ::_thesis: ex o1, o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
then  [a,b] in dom the Arrows of C by FUNCT_1:def_2;
then  [a,b] in [: the carrier of C, the carrier of C:] ;
then reconsider o1 = a, o2 = b as object of C by ZFMISC_1:87;
take  o1 ; ::_thesis: ex o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
take  o2 ; ::_thesis: ( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
thus  ( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 ) by A1, ALTCAT_1:def_1; ::_thesis: verum
end;

definition
let W be non empty set ;
defpred S1[ LATTICE] means $1 is complete ;
defpred S2[ LATTICE, LATTICE, Function of $1,$2] means $3 is infs-preserving ;
given w being Element of W such that A1: not w is empty ;
funcW -INF_category  ->  strict lattice-wise category means :Def4: :: WAYBEL34:def 4
( ( for x being LATTICE holds
( x is object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of it
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) );
existence
 ex b1 being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) )
proof
reconsider w = w as non empty set by A1;
set r = the well-ordering upper-bounded Order of w;
 RelStr(# w, the well-ordering upper-bounded Order of w #) is complete ;
then A2: ex x being strict LATTICE st
( S1[x] & the carrier of x in W ) ;
A3: for a, b, c being LATTICE st S1[a] & S1[b] & S1[c] holds
for f being Function of a,b
for g being Function of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f] by WAYBEL20:25;
A4: for a being LATTICE st S1[a] holds
S2[a,a, id a] ;
thus  ex C being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of C iff ( x is strict & S1[x] & the carrier of x in W ) ) ) & ( for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S2[ latt a, latt b,f] ) ) ) from YELLOW21:sch_3(A2, A3, A4); ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds
( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) & ( for x being LATTICE holds
( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) holds
b1 = b2
proof
let C1, C2 be strict lattice-wise category; ::_thesis: ( ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) implies C1 = C2 )
assume that
A5: for x being LATTICE holds
( x is object of C1 iff ( x is strict & S1[x] & the carrier of x in W ) ) and
A6: for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) and
A7: for x being LATTICE holds
( x is object of C2 iff ( x is strict & S1[x] & the carrier of x in W ) ) and
A8: for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ; ::_thesis: C1 = C2
defpred S3[ set , set , set ] means  ex L1, L2 being LATTICE ex f being Function of L1,L2 st
( $1 = L1 & $2 = L2 & $3 = f & f is infs-preserving );
A9: now__::_thesis:_for_a,_b_being_object_of_C1
for_f_being_monotone_Function_of_(latt_a),(latt_b)_holds_
(_f_in_<^a,b^>_iff_S3[a,b,f]_)
let a, b be object of C1; ::_thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )
let f be monotone Function of (latt a),(latt b); ::_thesis: ( f in <^a,b^> iff S3[a,b,f] )
 ( f in <^a,b^> iff f is infs-preserving ) by A6;
hence  ( f in <^a,b^> iff S3[a,b,f] ) ; ::_thesis: verum
end;
A10: now__::_thesis:_for_a,_b_being_object_of_C2
for_f_being_monotone_Function_of_(latt_a),(latt_b)_holds_
(_f_in_<^a,b^>_iff_S3[a,b,f]_)
let a, b be object of C2; ::_thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )
let f be monotone Function of (latt a),(latt b); ::_thesis: ( f in <^a,b^> iff S3[a,b,f] )
 ( f in <^a,b^> iff f is infs-preserving ) by A8;
hence  ( f in <^a,b^> iff S3[a,b,f] ) ; ::_thesis: verum
end;
 for C1, C2 being lattice-wise category st ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & S1[x] & the carrier of x in W ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & S1[x] & the carrier of x in W ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] ) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW21:sch_5();
hence  C1 = C2 by A5, A7, A9, A10; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines -INF_category WAYBEL34:def_4_:_
 for W being non empty set st not for w being Element of W holds w is empty holds
for b2 being strict lattice-wise category holds
( b2 = W -INF_category iff ( ( for x being LATTICE holds
( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) ) );

Lm3:  for W being with_non-empty_element set
for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -INF_category) . (a,b) iff ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) & a is complete & b is complete & f is infs-preserving ) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -INF_category) . (a,b) iff ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) & a is complete & b is complete & f is infs-preserving ) )
A1: ex x being non empty set st x in W by SETFAM_1:def_10;
let a, b be LATTICE; ::_thesis: for f being Function of a,b holds
( f in the Arrows of (W -INF_category) . (a,b) iff ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) & a is complete & b is complete & f is infs-preserving ) )
let f be Function of a,b; ::_thesis: ( f in the Arrows of (W -INF_category) . (a,b) iff ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) & a is complete & b is complete & f is infs-preserving ) )
set A = W -INF_category ;
hereby  ::_thesis: ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) & a is complete & b is complete & f is infs-preserving implies f in the Arrows of (W -INF_category) . (a,b) )
assume  f in the Arrows of (W -INF_category) . (a,b) ; ::_thesis: ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) & a is complete & b is complete & f is infs-preserving )
then consider o1, o2 being object of (W -INF_category) such that
A2: o1 = a and
A3: o2 = b and
A4: f in <^o1,o2^> and
 f is Morphism of o1,o2 by Th12;
reconsider g = f as Morphism of o1,o2 by A4;
thus  ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) ) by A2, A3; ::_thesis: ( a is complete & b is complete & f is infs-preserving )
thus  ( a is complete & b is complete ) by A1, A2, A3, Def4; ::_thesis: f is infs-preserving
 @ g = f by A4, YELLOW21:def_7;
hence  f is infs-preserving by A1, A2, A3, A4, Def4; ::_thesis: verum
end;
assume that
A5: a in the carrier of (W -INF_category) and
A6: b in the carrier of (W -INF_category) ; ::_thesis: ( not a is complete or not b is complete or not f is infs-preserving or f in the Arrows of (W -INF_category) . (a,b) )
reconsider x = a, y = b as object of (W -INF_category) by A5, A6;
A7: latt x = a ;
A8: latt y = b ;
assume that
 a is complete and
 b is complete and
A9: f is infs-preserving ; ::_thesis: f in the Arrows of (W -INF_category) . (a,b)
 f in <^x,y^> by A1, A7, A8, A9, Def4;
hence  f in the Arrows of (W -INF_category) . (a,b) by ALTCAT_1:def_1; ::_thesis: verum
end;

definition
let W be non empty set ;
defpred S1[ LATTICE] means $1 is complete ;
defpred S2[ LATTICE, LATTICE, Function of $1,$2] means $3 is sups-preserving ;
given w being Element of W such that A1: not w is empty ;
funcW -SUP_category  ->  strict lattice-wise category means :Def5: :: WAYBEL34:def 5
( ( for x being LATTICE holds
( x is object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of it
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) );
existence
 ex b1 being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) )
proof
reconsider w = w as non empty set by A1;
set r = the well-ordering upper-bounded Order of w;
 RelStr(# w, the well-ordering upper-bounded Order of w #) is complete ;
then A2: ex x being strict LATTICE st
( S1[x] & the carrier of x in W ) ;
A3: for a, b, c being LATTICE st S1[a] & S1[b] & S1[c] holds
for f being Function of a,b
for g being Function of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f] by WAYBEL20:27;
A4: for a being LATTICE st S1[a] holds
S2[a,a, id a] ;
thus  ex C being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of C iff ( x is strict & S1[x] & the carrier of x in W ) ) ) & ( for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S2[ latt a, latt b,f] ) ) ) from YELLOW21:sch_3(A2, A3, A4); ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds
( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) & ( for x being LATTICE holds
( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) holds
b1 = b2
proof
let C1, C2 be strict lattice-wise category; ::_thesis: ( ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) implies C1 = C2 )
assume that
A5: for x being LATTICE holds
( x is object of C1 iff ( x is strict & S1[x] & the carrier of x in W ) ) and
A6: for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) and
A7: for x being LATTICE holds
( x is object of C2 iff ( x is strict & S1[x] & the carrier of x in W ) ) and
A8: for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ; ::_thesis: C1 = C2
defpred S3[ set , set , set ] means  ex L1, L2 being LATTICE ex f being Function of L1,L2 st
( $1 = L1 & $2 = L2 & $3 = f & f is sups-preserving );
A9: now__::_thesis:_for_a,_b_being_object_of_C1
for_f_being_monotone_Function_of_(latt_a),(latt_b)_holds_
(_f_in_<^a,b^>_iff_S3[a,b,f]_)
let a, b be object of C1; ::_thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )
let f be monotone Function of (latt a),(latt b); ::_thesis: ( f in <^a,b^> iff S3[a,b,f] )
 ( f in <^a,b^> iff f is sups-preserving ) by A6;
hence  ( f in <^a,b^> iff S3[a,b,f] ) ; ::_thesis: verum
end;
A10: now__::_thesis:_for_a,_b_being_object_of_C2
for_f_being_monotone_Function_of_(latt_a),(latt_b)_holds_
(_f_in_<^a,b^>_iff_S3[a,b,f]_)
let a, b be object of C2; ::_thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )
let f be monotone Function of (latt a),(latt b); ::_thesis: ( f in <^a,b^> iff S3[a,b,f] )
 ( f in <^a,b^> iff f is sups-preserving ) by A8;
hence  ( f in <^a,b^> iff S3[a,b,f] ) ; ::_thesis: verum
end;
 for C1, C2 being lattice-wise category st ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & S1[x] & the carrier of x in W ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & S1[x] & the carrier of x in W ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] ) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW21:sch_5();
hence  C1 = C2 by A5, A7, A9, A10; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines -SUP_category WAYBEL34:def_5_:_
 for W being non empty set st not for w being Element of W holds w is empty holds
for b2 being strict lattice-wise category holds
( b2 = W -SUP_category iff ( ( for x being LATTICE holds
( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) ) );

Lm4:  for W being with_non-empty_element set
for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving ) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving ) )
A1: ex x being non empty set st x in W by SETFAM_1:def_10;
let a, b be LATTICE; ::_thesis: for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving ) )
let f be Function of a,b; ::_thesis: ( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving ) )
set A = W -SUP_category ;
hereby  ::_thesis: ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving implies f in the Arrows of (W -SUP_category) . (a,b) )
assume  f in the Arrows of (W -SUP_category) . (a,b) ; ::_thesis: ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving )
then consider o1, o2 being object of (W -SUP_category) such that
A2: o1 = a and
A3: o2 = b and
A4: f in <^o1,o2^> and
 f is Morphism of o1,o2 by Th12;
reconsider g = f as Morphism of o1,o2 by A4;
thus  ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) ) by A2, A3; ::_thesis: ( a is complete & b is complete & f is sups-preserving )
thus  ( a is complete & b is complete ) by A1, A2, A3, Def5; ::_thesis: f is sups-preserving
 @ g = f by A4, YELLOW21:def_7;
hence  f is sups-preserving by A1, A2, A3, A4, Def5; ::_thesis: verum
end;
assume that
A5: a in the carrier of (W -SUP_category) and
A6: b in the carrier of (W -SUP_category) ; ::_thesis: ( not a is complete or not b is complete or not f is sups-preserving or f in the Arrows of (W -SUP_category) . (a,b) )
reconsider x = a, y = b as object of (W -SUP_category) by A5, A6;
A7: latt x = a ;
A8: latt y = b ;
assume that
 a is complete and
 b is complete and
A9: f is sups-preserving ; ::_thesis: f in the Arrows of (W -SUP_category) . (a,b)
 f in <^x,y^> by A1, A7, A8, A9, Def5;
hence  f in the Arrows of (W -SUP_category) . (a,b) by ALTCAT_1:def_1; ::_thesis: verum
end;

registration
let W be with_non-empty_element set ;
clusterW -INF_category  ->  strict lattice-wise with_complete_lattices ;
coherence
 W -INF_category is with_complete_lattices
proof
thus  W -INF_category is lattice-wise ; :: according to YELLOW21:def_5 ::_thesis: for b1 being Element of the carrier of (W -INF_category) holds b1 is RelStr
let a be object of (W -INF_category); ::_thesis: a is RelStr
A1: ex x being non empty set st x in W by SETFAM_1:def_10;
 a = latt a ;
hence  a is RelStr by A1, Def4; ::_thesis: verum
end;
clusterW -SUP_category  ->  strict lattice-wise with_complete_lattices ;
coherence
 W -SUP_category is with_complete_lattices
proof
thus  W -SUP_category is lattice-wise ; :: according to YELLOW21:def_5 ::_thesis: for b1 being Element of the carrier of (W -SUP_category) holds b1 is RelStr
let a be object of (W -SUP_category); ::_thesis: a is RelStr
A2: ex x being non empty set st x in W by SETFAM_1:def_10;
 a = latt a ;
hence  a is RelStr by A2, Def5; ::_thesis: verum
end;
end;

theorem Th13: :: WAYBEL34:13
for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -INF_category) iff ( L is strict & L is complete & the carrier of L in W ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE holds
( L is object of (W -INF_category) iff ( L is strict & L is complete & the carrier of L in W ) )
 ex a being non empty set st a in W by SETFAM_1:def_10;
hence  for L being LATTICE holds
( L is object of (W -INF_category) iff ( L is strict & L is complete & the carrier of L in W ) ) by Def4; ::_thesis: verum
end;

theorem Th14: :: WAYBEL34:14
for W being with_non-empty_element set
for a, b being object of (W -INF_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -INF_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
let a, b be object of (W -INF_category); ::_thesis: for f being set holds
( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
let f be set ; ::_thesis: ( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
A1: ex a being non empty set st a in W by SETFAM_1:def_10;
hereby  ::_thesis: ( f is infs-preserving Function of (latt a),(latt b) implies f in <^a,b^> )
assume A2: f in <^a,b^> ; ::_thesis: f is infs-preserving Function of (latt a),(latt b)
then reconsider g = f as Morphism of a,b ;
 f = @ g by A2, YELLOW21:def_7;
hence  f is infs-preserving Function of (latt a),(latt b) by A1, A2, Def4; ::_thesis: verum
end;
thus  ( f is infs-preserving Function of (latt a),(latt b) implies f in <^a,b^> ) by A1, Def4; ::_thesis: verum
end;

theorem Th15: :: WAYBEL34:15
for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -SUP_category) iff ( L is strict & L is complete & the carrier of L in W ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE holds
( L is object of (W -SUP_category) iff ( L is strict & L is complete & the carrier of L in W ) )
 ex a being non empty set st a in W by SETFAM_1:def_10;
hence  for L being LATTICE holds
( L is object of (W -SUP_category) iff ( L is strict & L is complete & the carrier of L in W ) ) by Def5; ::_thesis: verum
end;

theorem Th16: :: WAYBEL34:16
for W being with_non-empty_element set
for a, b being object of (W -SUP_category)
for f being set holds
( f in <^a,b^> iff f is sups-preserving Function of (latt a),(latt b) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -SUP_category)
for f being set holds
( f in <^a,b^> iff f is sups-preserving Function of (latt a),(latt b) )
let a, b be object of (W -SUP_category); ::_thesis: for f being set holds
( f in <^a,b^> iff f is sups-preserving Function of (latt a),(latt b) )
let f be set ; ::_thesis: ( f in <^a,b^> iff f is sups-preserving Function of (latt a),(latt b) )
A1: ex a being non empty set st a in W by SETFAM_1:def_10;
hereby  ::_thesis: ( f is sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> )
assume A2: f in <^a,b^> ; ::_thesis: f is sups-preserving Function of (latt a),(latt b)
then reconsider g = f as Morphism of a,b ;
 f = @ g by A2, YELLOW21:def_7;
hence  f is sups-preserving Function of (latt a),(latt b) by A1, A2, Def5; ::_thesis: verum
end;
thus  ( f is sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> ) by A1, Def5; ::_thesis: verum
end;

theorem Th17: :: WAYBEL34:17
for W being with_non-empty_element set holds the carrier of (W -INF_category) = the carrier of (W -SUP_category)
proof
let W be with_non-empty_element set ; ::_thesis: the carrier of (W -INF_category) = the carrier of (W -SUP_category)
A1: ex x being non empty set st x in W by SETFAM_1:def_10;
thus  the carrier of (W -INF_category) c= the carrier of (W -SUP_category) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (W -SUP_category) c= the carrier of (W -INF_category)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W -INF_category) or x in the carrier of (W -SUP_category) )
assume A2: x in the carrier of (W -INF_category) ; ::_thesis: x in the carrier of (W -SUP_category)
then reconsider x = x as LATTICE by YELLOW21:def_4;
A3: ( x is strict & x is complete ) by A1, A2, Def4;
 the carrier of x in W by A1, A2, Def4;
then  x is object of (W -SUP_category) by A3, Def5;
hence  x in the carrier of (W -SUP_category) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W -SUP_category) or x in the carrier of (W -INF_category) )
assume A4: x in the carrier of (W -SUP_category) ; ::_thesis: x in the carrier of (W -INF_category)
then reconsider x = x as LATTICE by YELLOW21:def_4;
A5: ( x is strict & x is complete ) by A1, A4, Def5;
 the carrier of x in W by A1, A4, Def5;
then  x is object of (W -INF_category) by A5, Def4;
hence  x in the carrier of (W -INF_category) ; ::_thesis: verum
end;

definition
let W be with_non-empty_element set ;
set A = W -INF_category ;
set B = W -SUP_category ;
deffunc H1( LATTICE) ->  LATTICE = $1;
deffunc H2( LATTICE, LATTICE, Function of $1,$2) ->  Function of $2,$1 = LowerAdj $3;
defpred S1[ LATTICE, LATTICE, Function of $1,$2] means ( $1 is complete & $2 is complete & $3 is infs-preserving );
defpred S2[ LATTICE, LATTICE, Function of $1,$2] means ( $1 is complete & $2 is complete & $3 is sups-preserving );
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -INF_category) . (a,b) iff ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) & S1[a,b,f] ) ) by Lm3;
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & S2[a,b,f] ) ) by Lm4;
A3: for a being LATTICE st a in the carrier of (W -INF_category) holds
H1(a) in the carrier of (W -SUP_category) by Th17;
A4: for a, b being LATTICE
for f being Function of a,b st S1[a,b,f] holds
( H2(a,b,f) is Function of H1(b),H1(a) & S2[H1(b),H1(a),H2(a,b,f)] ) ;
A5: now__::_thesis:_for_a_being_LATTICE_st_a_in_the_carrier_of_(W_-INF_category)_holds_
H2(a,a,_id_a)_=_id_H1(a)
let a be LATTICE; ::_thesis: ( a in the carrier of (W -INF_category) implies H2(a,a, id a) = id H1(a) )
assume  a in the carrier of (W -INF_category) ; ::_thesis: H2(a,a, id a) = id H1(a)
then  a is complete by YELLOW21:def_5;
hence  H2(a,a, id a) = id H1(a) by Th7; ::_thesis: verum
end;
A6: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st S1[a,b,f] & S1[b,c,g] holds
H2(a,c,g * f) = H2(a,b,f) * H2(b,c,g) by Th8;
funcW LowerAdj  ->  strict contravariant Functor of W -INF_category ,W -SUP_category  means :Def6: :: WAYBEL34:def 6
( ( for a being object of (W -INF_category) holds it . a = latt a ) & ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds it . f = LowerAdj (@ f) ) );
existence
 ex b1 being strict contravariant Functor of W -INF_category ,W -SUP_category st
( ( for a being object of (W -INF_category) holds b1 . a = latt a ) & ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = LowerAdj (@ f) ) )
proof
thus  ex F being strict contravariant Functor of W -INF_category ,W -SUP_category st
( ( for a being object of (W -INF_category) holds F . a = H1( latt a) ) & ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = H2( latt a, latt b, @ f) ) ) from YELLOW21:sch_7(A1, A2, A3, A4, A5, A6); ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict contravariant Functor of W -INF_category ,W -SUP_category st ( for a being object of (W -INF_category) holds b1 . a = latt a ) & ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = LowerAdj (@ f) ) & ( for a being object of (W -INF_category) holds b2 . a = latt a ) & ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = LowerAdj (@ f) ) holds
b1 = b2
proof
let F, G be strict contravariant Functor of W -INF_category ,W -SUP_category ; ::_thesis: ( ( for a being object of (W -INF_category) holds F . a = latt a ) & ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = LowerAdj (@ f) ) & ( for a being object of (W -INF_category) holds G . a = latt a ) & ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = LowerAdj (@ f) ) implies F = G )
assume that
A7: for a being object of (W -INF_category) holds F . a = latt a and
A8: for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = LowerAdj (@ f) and
A9: for a being object of (W -INF_category) holds G . a = latt a and
A10: for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = LowerAdj (@ f) ; ::_thesis: F = G
A11: now__::_thesis:_for_a_being_object_of_(W_-INF_category)_holds_F_._a_=_G_._a
let a be object of (W -INF_category); ::_thesis: F . a = G . a
thus F . a = latt a by A7
.= G . a by A9 ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_object_of_(W_-INF_category)_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_F_._f_=_G_._f
let a, b be object of (W -INF_category); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )
assume A12: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F . f = G . f
let f be Morphism of a,b; ::_thesis: F . f = G . f
thus F . f = LowerAdj (@ f) by A8, A12
.= G . f by A10, A12 ; ::_thesis: verum
end;
hence  F = G by A11, YELLOW18:2; ::_thesis: verum
end;
deffunc H3( LATTICE, LATTICE, Function of $1,$2) ->  Function of $2,$1 = UpperAdj $3;
A13: for a being LATTICE st a in the carrier of (W -SUP_category) holds
H1(a) in the carrier of (W -INF_category) by Th17;
A14: for a, b being LATTICE
for f being Function of a,b st S2[a,b,f] holds
( H3(a,b,f) is Function of H1(b),H1(a) & S1[H1(b),H1(a),H3(a,b,f)] ) ;
A15: now__::_thesis:_for_a_being_LATTICE_st_a_in_the_carrier_of_(W_-SUP_category)_holds_
H3(a,a,_id_a)_=_id_H1(a)
let a be LATTICE; ::_thesis: ( a in the carrier of (W -SUP_category) implies H3(a,a, id a) = id H1(a) )
assume  a in the carrier of (W -SUP_category) ; ::_thesis: H3(a,a, id a) = id H1(a)
then  a is complete by YELLOW21:def_5;
hence  H3(a,a, id a) = id H1(a) by Th7; ::_thesis: verum
end;
A16: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st S2[a,b,f] & S2[b,c,g] holds
H3(a,c,g * f) = H3(a,b,f) * H3(b,c,g) by Th9;
funcW UpperAdj  ->  strict contravariant Functor of W -SUP_category ,W -INF_category  means :Def7: :: WAYBEL34:def 7
( ( for a being object of (W -SUP_category) holds it . a = latt a ) & ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds it . f = UpperAdj (@ f) ) );
existence
 ex b1 being strict contravariant Functor of W -SUP_category ,W -INF_category st
( ( for a being object of (W -SUP_category) holds b1 . a = latt a ) & ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = UpperAdj (@ f) ) )
proof
thus  ex F being strict contravariant Functor of W -SUP_category ,W -INF_category st
( ( for a being object of (W -SUP_category) holds F . a = H1( latt a) ) & ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = H3( latt a, latt b, @ f) ) ) from YELLOW21:sch_7(A2, A1, A13, A14, A15, A16); ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict contravariant Functor of W -SUP_category ,W -INF_category st ( for a being object of (W -SUP_category) holds b1 . a = latt a ) & ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = UpperAdj (@ f) ) & ( for a being object of (W -SUP_category) holds b2 . a = latt a ) & ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = UpperAdj (@ f) ) holds
b1 = b2
proof
let F, G be strict contravariant Functor of W -SUP_category ,W -INF_category ; ::_thesis: ( ( for a being object of (W -SUP_category) holds F . a = latt a ) & ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = UpperAdj (@ f) ) & ( for a being object of (W -SUP_category) holds G . a = latt a ) & ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = UpperAdj (@ f) ) implies F = G )
assume that
A17: for a being object of (W -SUP_category) holds F . a = latt a and
A18: for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = UpperAdj (@ f) and
A19: for a being object of (W -SUP_category) holds G . a = latt a and
A20: for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = UpperAdj (@ f) ; ::_thesis: F = G
A21: now__::_thesis:_for_a_being_object_of_(W_-SUP_category)_holds_F_._a_=_G_._a
let a be object of (W -SUP_category); ::_thesis: F . a = G . a
thus F . a = latt a by A17
.= G . a by A19 ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_object_of_(W_-SUP_category)_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_F_._f_=_G_._f
let a, b be object of (W -SUP_category); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )
assume A22: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F . f = G . f
let f be Morphism of a,b; ::_thesis: F . f = G . f
thus F . f = UpperAdj (@ f) by A18, A22
.= G . f by A20, A22 ; ::_thesis: verum
end;
hence  F = G by A21, YELLOW18:2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines LowerAdj WAYBEL34:def_6_:_
 for W being with_non-empty_element set
for b2 being strict contravariant Functor of W -INF_category ,W -SUP_category holds
( b2 = W LowerAdj iff ( ( for a being object of (W -INF_category) holds b2 . a = latt a ) & ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = LowerAdj (@ f) ) ) );

:: deftheorem Def7 defines UpperAdj WAYBEL34:def_7_:_
 for W being with_non-empty_element set
for b2 being strict contravariant Functor of W -SUP_category ,W -INF_category holds
( b2 = W UpperAdj iff ( ( for a being object of (W -SUP_category) holds b2 . a = latt a ) & ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = UpperAdj (@ f) ) ) );

registration
let W be with_non-empty_element set ;
clusterW LowerAdj  ->  strict contravariant bijective ;
coherence
 W LowerAdj is bijective
proof
set A = W -INF_category ;
set B = W -SUP_category ;
set F = W LowerAdj ;
A1: ex x being non empty set st x in W by SETFAM_1:def_10;
deffunc H1( object of (W -INF_category)) ->  RelStr = latt W;
deffunc H2( object of (W -INF_category), object of (W -INF_category), Morphism of W,c2) ->  Function of (latt c2),(latt W) = LowerAdj (@ c3);
A2: for a being object of (W -INF_category) holds (W LowerAdj) . a = H1(a) by Def6;
A3: for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W LowerAdj) . f = H2(a,b,f) by Def6;
A4: for a, b being object of (W -INF_category) st H1(a) = H1(b) holds
a = b ;
A5: now__::_thesis:_for_a,_b_being_object_of_(W_-INF_category)_st_<^a,b^>_<>_{}_holds_
for_f,_g_being_Morphism_of_a,b_st_H2(a,b,f)_=_H2(a,b,g)_holds_
f_=_g
let a, b be object of (W -INF_category); ::_thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g )
assume A6: <^a,b^> <> {} ; ::_thesis: for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g
let f, g be Morphism of a,b; ::_thesis: ( H2(a,b,f) = H2(a,b,g) implies f = g )
A7: @ f = f by A6, YELLOW21:def_7;
A8: @ g = g by A6, YELLOW21:def_7;
A9: latt a is complete ;
A10: latt b is complete ;
A11: @ f is infs-preserving by A1, A6, A7, Def4;
A12: @ g is infs-preserving by A1, A6, A8, Def4;
assume  H2(a,b,f) = H2(a,b,g) ; ::_thesis: f = g
hence f = UpperAdj (LowerAdj (@ g)) by A7, A9, A10, A11, Th10
.= g by A8, A9, A10, A12, Th10 ;
::_thesis: verum
end;
A13: now__::_thesis:_for_a,_b_being_object_of_(W_-SUP_category)_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_ex_c,_d_being_object_of_(W_-INF_category)_ex_g_being_Morphism_of_c,d_st_
(_b_=_H1(c)_&_a_=_H1(d)_&_<^c,d^>_<>_{}_&_f_=_H2(c,d,g)_)
let a, b be object of (W -SUP_category); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of (W -INF_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) ) )
assume A14: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b ex c, d being object of (W -INF_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
let f be Morphism of a,b; ::_thesis: ex c, d being object of (W -INF_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
A15: ( latt a is strict & latt a is complete ) by A1, Def5;
A16: the carrier of (latt a) in W by A1, Def5;
A17: ( latt b is strict & latt b is complete ) by A1, Def5;
 the carrier of (latt b) in W by A1, Def5;
then reconsider c = latt b, d = latt a as object of (W -INF_category) by A15, A16, A17, Def4;
take c = c; ::_thesis: ex d being object of (W -INF_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
take d = d; ::_thesis: ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
A18: latt c = c ;
A19: latt d = d ;
A20: f = @ f by A14, YELLOW21:def_7;
then A21: @ f is sups-preserving by A1, A14, Def5;
then A22: ( UpperAdj (@ f) is monotone & UpperAdj (@ f) is infs-preserving ) by A18, A19;
A23: UpperAdj (@ f) in <^c,d^> by A1, A21, Def4;
reconsider g = UpperAdj (@ f) as Morphism of c,d by A1, A21, Def4;
take g = g; ::_thesis: ( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
thus  ( b = H1(c) & a = H1(d) & <^c,d^> <> {} ) by A1, A22, Def4; ::_thesis: f = H2(c,d,g)
 g = @ g by A23, YELLOW21:def_7;
hence  f = H2(c,d,g) by A20, A21, Th11; ::_thesis: verum
end;
thus  W LowerAdj is bijective from YELLOW18:sch_12(A2, A3, A4, A5, A13); ::_thesis: verum
end;
clusterW UpperAdj  ->  strict contravariant bijective ;
coherence
 W UpperAdj is bijective
proof
set A = W -SUP_category ;
set B = W -INF_category ;
set F = W UpperAdj ;
A24: ex x being non empty set st x in W by SETFAM_1:def_10;
deffunc H1( object of (W -SUP_category)) ->  RelStr = latt W;
deffunc H2( object of (W -SUP_category), object of (W -SUP_category), Morphism of W,c2) ->  Function of (latt c2),(latt W) = UpperAdj (@ c3);
A25: for a being object of (W -SUP_category) holds (W UpperAdj) . a = H1(a) by Def7;
A26: for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W UpperAdj) . f = H2(a,b,f) by Def7;
A27: for a, b being object of (W -SUP_category) st H1(a) = H1(b) holds
a = b ;
A28: now__::_thesis:_for_a,_b_being_object_of_(W_-SUP_category)_st_<^a,b^>_<>_{}_holds_
for_f,_g_being_Morphism_of_a,b_st_H2(a,b,f)_=_H2(a,b,g)_holds_
f_=_g
let a, b be object of (W -SUP_category); ::_thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g )
assume A29: <^a,b^> <> {} ; ::_thesis: for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g
let f, g be Morphism of a,b; ::_thesis: ( H2(a,b,f) = H2(a,b,g) implies f = g )
A30: @ f = f by A29, YELLOW21:def_7;
A31: @ g = g by A29, YELLOW21:def_7;
A32: latt a is complete ;
A33: latt b is complete ;
A34: @ f is sups-preserving by A24, A29, A30, Def5;
A35: @ g is sups-preserving by A24, A29, A31, Def5;
assume  H2(a,b,f) = H2(a,b,g) ; ::_thesis: f = g
hence f = LowerAdj (UpperAdj (@ g)) by A30, A32, A33, A34, Th11
.= g by A31, A32, A33, A35, Th11 ;
::_thesis: verum
end;
A36: now__::_thesis:_for_a,_b_being_object_of_(W_-INF_category)_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_ex_c,_d_being_object_of_(W_-SUP_category)_ex_g_being_Morphism_of_c,d_st_
(_b_=_H1(c)_&_a_=_H1(d)_&_<^c,d^>_<>_{}_&_f_=_H2(c,d,g)_)
let a, b be object of (W -INF_category); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) ) )
assume A37: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b ex c, d being object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
let f be Morphism of a,b; ::_thesis: ex c, d being object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
A38: ( latt a is strict & latt a is complete ) by A24, Def4;
A39: the carrier of (latt a) in W by A24, Def4;
A40: ( latt b is strict & latt b is complete ) by A24, Def4;
 the carrier of (latt b) in W by A24, Def4;
then reconsider c = latt b, d = latt a as object of (W -SUP_category) by A38, A39, A40, Def5;
take c = c; ::_thesis: ex d being object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
take d = d; ::_thesis: ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
A41: latt c = c ;
A42: latt d = d ;
A43: f = @ f by A37, YELLOW21:def_7;
then A44: @ f is infs-preserving by A24, A37, Def4;
then A45: ( LowerAdj (@ f) is monotone & LowerAdj (@ f) is sups-preserving ) by A41, A42;
A46: LowerAdj (@ f) in <^c,d^> by A24, A44, Def5;
reconsider g = LowerAdj (@ f) as Morphism of c,d by A24, A44, Def5;
take g = g; ::_thesis: ( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
thus  ( b = H1(c) & a = H1(d) & <^c,d^> <> {} ) by A24, A45, Def5; ::_thesis: f = H2(c,d,g)
 g = @ g by A46, YELLOW21:def_7;
hence  f = H2(c,d,g) by A43, A44, Th10; ::_thesis: verum
end;
thus  W UpperAdj is bijective from YELLOW18:sch_12(A25, A26, A27, A28, A36); ::_thesis: verum
end;
end;

theorem Th18: :: WAYBEL34:18
for W being with_non-empty_element set holds
( (W LowerAdj) " = W UpperAdj & (W UpperAdj) " = W LowerAdj )
proof
let W be with_non-empty_element set ; ::_thesis: ( (W LowerAdj) " = W UpperAdj & (W UpperAdj) " = W LowerAdj )
A1: ex x being non empty set st x in W by SETFAM_1:def_10;
set B = W -SUP_category ;
set F = W LowerAdj ;
set G = W UpperAdj ;
A2: now__::_thesis:_for_a_being_object_of_(W_-SUP_category)_holds_(W_LowerAdj)_._((W_UpperAdj)_._a)_=_a
let a be object of (W -SUP_category); ::_thesis: (W LowerAdj) . ((W UpperAdj) . a) = a
thus (W LowerAdj) . ((W UpperAdj) . a) = latt ((W UpperAdj) . a) by Def6
.= latt a by Def7
.= a ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_object_of_(W_-SUP_category)_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_(W_LowerAdj)_._((W_UpperAdj)_._f)_=_f
let a, b be object of (W -SUP_category); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (W LowerAdj) . ((W UpperAdj) . f) = f )
assume A3: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds (W LowerAdj) . ((W UpperAdj) . f) = f
then A4: <^((W UpperAdj) . b),((W UpperAdj) . a)^> <> {} by FUNCTOR0:def_19;
let f be Morphism of a,b; ::_thesis: (W LowerAdj) . ((W UpperAdj) . f) = f
A5: (W UpperAdj) . f = UpperAdj (@ f) by A3, Def7;
A6: @ f = f by A3, YELLOW21:def_7;
A7: @ ((W UpperAdj) . f) = (W UpperAdj) . f by A4, YELLOW21:def_7;
A8: (W UpperAdj) . a = latt a by Def7;
A9: (W UpperAdj) . b = latt b by Def7;
A10: @ f is sups-preserving by A1, A3, A6, Def5;
thus (W LowerAdj) . ((W UpperAdj) . f) = LowerAdj (@ ((W UpperAdj) . f)) by A4, Def6
.= f by A5, A6, A7, A8, A9, A10, Th11 ; ::_thesis: verum
end;
hence  (W LowerAdj) " = W UpperAdj by A2, YELLOW20:7; ::_thesis: (W UpperAdj) " = W LowerAdj
set B = W -INF_category ;
set G = W LowerAdj ;
set F = W UpperAdj ;
A11: now__::_thesis:_for_a_being_object_of_(W_-INF_category)_holds_(W_UpperAdj)_._((W_LowerAdj)_._a)_=_a
let a be object of (W -INF_category); ::_thesis: (W UpperAdj) . ((W LowerAdj) . a) = a
thus (W UpperAdj) . ((W LowerAdj) . a) = latt ((W LowerAdj) . a) by Def7
.= latt a by Def6
.= a ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_object_of_(W_-INF_category)_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_(W_UpperAdj)_._((W_LowerAdj)_._f)_=_f
let a, b be object of (W -INF_category); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (W UpperAdj) . ((W LowerAdj) . f) = f )
assume A12: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds (W UpperAdj) . ((W LowerAdj) . f) = f
then A13: <^((W LowerAdj) . b),((W LowerAdj) . a)^> <> {} by FUNCTOR0:def_19;
let f be Morphism of a,b; ::_thesis: (W UpperAdj) . ((W LowerAdj) . f) = f
A14: (W LowerAdj) . f = LowerAdj (@ f) by A12, Def6;
A15: @ f = f by A12, YELLOW21:def_7;
A16: @ ((W LowerAdj) . f) = (W LowerAdj) . f by A13, YELLOW21:def_7;
A17: (W LowerAdj) . a = latt a by Def6;
A18: (W LowerAdj) . b = latt b by Def6;
A19: @ f is infs-preserving by A1, A12, A15, Def4;
thus (W UpperAdj) . ((W LowerAdj) . f) = UpperAdj (@ ((W LowerAdj) . f)) by A13, Def7
.= f by A14, A15, A16, A17, A18, A19, Th10 ; ::_thesis: verum
end;
hence  (W UpperAdj) " = W LowerAdj by A11, YELLOW20:7; ::_thesis: verum
end;

theorem :: WAYBEL34:19
for W being with_non-empty_element set holds
( (W LowerAdj) * (W UpperAdj) = id (W -SUP_category) & (W UpperAdj) * (W LowerAdj) = id (W -INF_category) )
proof
let W be with_non-empty_element set ; ::_thesis: ( (W LowerAdj) * (W UpperAdj) = id (W -SUP_category) & (W UpperAdj) * (W LowerAdj) = id (W -INF_category) )
A1: (W LowerAdj) " = W UpperAdj by Th18;
 (W UpperAdj) " = W LowerAdj by Th18;
hence  ( (W LowerAdj) * (W UpperAdj) = id (W -SUP_category) & (W UpperAdj) * (W LowerAdj) = id (W -INF_category) ) by A1, FUNCTOR1:18; ::_thesis: verum
end;

theorem :: WAYBEL34:20
for W being with_non-empty_element set holds W -INF_category ,W -SUP_category are_anti-isomorphic
proof
let W be with_non-empty_element set ; ::_thesis: W -INF_category ,W -SUP_category are_anti-isomorphic
take  W LowerAdj ; :: according to FUNCTOR0:def_40 ::_thesis: ( W LowerAdj is bijective & W LowerAdj is contravariant )
thus  ( W LowerAdj is bijective & W LowerAdj is contravariant ) ; ::_thesis: verum
end;

begin

theorem Th21: :: WAYBEL34:21
for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y )
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y )
let g be infs-preserving Function of S,T; ::_thesis: ( g is directed-sups-preserving iff for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y )
hereby  ::_thesis: ( ( for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) implies g is directed-sups-preserving )
assume A1: g is directed-sups-preserving ; ::_thesis: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y
let X be Scott TopAugmentation of T; ::_thesis: for Y being Scott TopAugmentation of S
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y
let Y be Scott TopAugmentation of S; ::_thesis: for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y
let V be open Subset of X; ::_thesis: uparrow ((LowerAdj g) .: V) is open Subset of Y
A2: RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A3: RelStr(# the carrier of Y, the InternalRel of Y #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then reconsider g9 = g as Function of Y,X by A2;
reconsider d = LowerAdj g as Function of X,Y by A2, A3;
 uparrow (d .: V) is inaccessible
proof
let D be non empty directed Subset of Y; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,Y) in uparrow (d .: V) or not D misses uparrow (d .: V) )
assume  sup D in uparrow (d .: V) ; ::_thesis: not D misses uparrow (d .: V)
then consider y being Element of Y such that
A4: y <= sup D and
A5: y in d .: V by WAYBEL_0:def_16;
consider u being set  such that
A6: u in the carrier of X and
A7: u in V and
A8: y = d . u by A5, FUNCT_2:64;
reconsider u = u as Element of X by A6;
reconsider g = g9 as Function of Y,X ;
 [g,d] is Galois Connection of S,T by Def1;
then A9: [g,d] is Galois by A2, A3, Th1;
then A10: d * g <= id Y by WAYBEL_1:18;
A11: id X <= g * d by A9, WAYBEL_1:18;
A12: (id X) . u = u by FUNCT_1:18;
A13: (g * d) . u = g . (d . u) by FUNCT_2:15;
A14: g is infs-preserving Function of Y,X by A2, A3, WAYBEL21:6;
A15: u <= g . y by A8, A11, A12, A13, YELLOW_2:9;
 g . y <= g . (sup D) by A4, A14, ORDERS_3:def_5;
then A16: u <= g . (sup D) by A15, ORDERS_2:3;
 V is upper by WAYBEL11:def_4;
then A17: g . (sup D) in V by A7, A16, WAYBEL_0:def_20;
 g is directed-sups-preserving by A1, A2, A3, WAYBEL21:6;
then A18: g preserves_sup_of D by WAYBEL_0:def_37;
 ex_sup_of D,Y by YELLOW_0:17;
then A19: g . (sup D) = sup (g .: D) by A18, WAYBEL_0:def_31;
A20: ( g .: D is directed & not g .: D is empty ) by A14, YELLOW_2:15;
 V is inaccessible by WAYBEL11:def_4;
then  g .: D meets V by A17, A19, A20, WAYBEL11:def_1;
then consider z being set  such that
A21: z in g .: D and
A22: z in V by XBOOLE_0:3;
consider x being set  such that
A23: x in the carrier of Y and
A24: x in D and
A25: z = g . x by A21, FUNCT_2:64;
reconsider x = x as Element of Y by A23;
A26: (d * g) . x = d . (g . x) by FUNCT_2:15;
 (id Y) . x = x by FUNCT_1:18;
then A27: d . (g . x) <= x by A10, A26, YELLOW_2:9;
 d . z in d .: V by A22, FUNCT_2:35;
then  x in uparrow (d .: V) by A25, A27, WAYBEL_0:def_16;
hence  not D misses uparrow (d .: V) by A24, XBOOLE_0:3; ::_thesis: verum
end;
then  uparrow (d .: V) is open Subset of Y by WAYBEL11:def_4;
hence  uparrow ((LowerAdj g) .: V) is open Subset of Y by A3, WAYBEL_0:13; ::_thesis: verum
end;
assume A28: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ; ::_thesis: g is directed-sups-preserving
set X = the Scott TopAugmentation of T;
set Y = the Scott TopAugmentation of S;
A29: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A30: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then reconsider g9 = g as Function of the Scott TopAugmentation of S, the Scott TopAugmentation of T by A29;
reconsider g9 = g9 as infs-preserving Function of the Scott TopAugmentation of S, the Scott TopAugmentation of T by A29, A30, WAYBEL21:6;
set d = LowerAdj g;
reconsider d9 = LowerAdj g as Function of the Scott TopAugmentation of T, the Scott TopAugmentation of S by A29, A30;
let D be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or g preserves_sup_of D )
assume A31: ( not D is empty & D is directed ) ; ::_thesis: g preserves_sup_of D
assume  ex_sup_of D,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: D,T & "\/" ((g .: D),T) = g . ("\/" (D,S)) )
thus  ex_sup_of g .: D,T by YELLOW_0:17; ::_thesis: "\/" ((g .: D),T) = g . ("\/" (D,S))
A32: sup (g .: D) <= g . (sup D) by WAYBEL17:15;
reconsider D9 = D as Subset of the Scott TopAugmentation of S by A30;
reconsider D9 = D9 as non empty directed Subset of the Scott TopAugmentation of S by A30, A31, WAYBEL_0:3;
reconsider s = sup D as Element of the Scott TopAugmentation of S by A30;
set U9 = (downarrow (sup (g9 .: D9))) ` ;
A33: (downarrow (sup (g9 .: D9))) ` is open by WAYBEL11:12;
then  uparrow ((LowerAdj g) .: ((downarrow (sup (g9 .: D9))) `)) is open Subset of the Scott TopAugmentation of S by A28;
then A34: uparrow ((LowerAdj g) .: ((downarrow (sup (g9 .: D9))) `)) is upper inaccessible Subset of the Scott TopAugmentation of S by WAYBEL11:def_4;
 sup (g9 .: D9) = sup (g .: D) by A29, YELLOW_0:17, YELLOW_0:26;
then A35: downarrow (sup (g9 .: D9)) = downarrow (sup (g .: D)) by A29, WAYBEL_0:13;
A36: sup (g .: D) <= sup (g .: D) ;
A37: [g,(LowerAdj g)] is Galois by Def1;
then A38: (LowerAdj g) * g <= id S by WAYBEL_1:18;
A39: id T <= g * (LowerAdj g) by A37, WAYBEL_1:18;
A40: (id S) . (sup D) = sup D by FUNCT_1:18;
 ((LowerAdj g) * g) . (sup D) = (LowerAdj g) . (g . (sup D)) by FUNCT_2:15;
then  (LowerAdj g) . (g . (sup D)) <= sup D by A38, A40, YELLOW_2:9;
then A41: d9 . (g9 . s) <= s by A30, YELLOW_0:1;
A42: s = sup D9 by A30, YELLOW_0:17, YELLOW_0:26;
 g . (sup D) <= sup (g .: D)
proof
assume  not g . (sup D) <= sup (g .: D) ; ::_thesis: contradiction
then A43: not g . (sup D) in downarrow (sup (g .: D)) by WAYBEL_0:17;
A44: sup (g .: D) in downarrow (sup (g .: D)) by A36, WAYBEL_0:17;
A45: g . (sup D) in (downarrow (sup (g9 .: D9))) ` by A29, A35, A43, XBOOLE_0:def_5;
A46: not sup (g .: D) in (downarrow (sup (g9 .: D9))) ` by A35, A44, XBOOLE_0:def_5;
A47: d9 . (g9 . s) in d9 .: ((downarrow (sup (g9 .: D9))) `) by A45, FUNCT_2:35;
 d9 .: ((downarrow (sup (g9 .: D9))) `) c= uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `)) by WAYBEL_0:16;
then A48: s in uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `)) by A41, A47, WAYBEL_0:def_20;
 uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `)) = uparrow ((LowerAdj g) .: ((downarrow (sup (g9 .: D9))) `)) by A30, WAYBEL_0:13;
then  D9 meets uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `)) by A34, A42, A48, WAYBEL11:def_1;
then consider x being set  such that
A49: x in D9 and
A50: x in uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `)) by XBOOLE_0:3;
reconsider x = x as Element of the Scott TopAugmentation of S by A49;
consider u9 being Element of the Scott TopAugmentation of S such that
A51: u9 <= x and
A52: u9 in d9 .: ((downarrow (sup (g9 .: D9))) `) by A50, WAYBEL_0:def_16;
consider u being set  such that
A53: u in the carrier of the Scott TopAugmentation of T and
A54: u in (downarrow (sup (g9 .: D9))) ` and
A55: u9 = d9 . u by A52, FUNCT_2:64;
reconsider u = u as Element of the Scott TopAugmentation of T by A53;
reconsider a = u as Element of T by A29;
 (id T) . a = u by FUNCT_1:18;
then  a <= (g * (LowerAdj g)) . a by A39, YELLOW_2:9;
then  a <= g . ((LowerAdj g) . a) by FUNCT_2:15;
then A56: u <= g9 . (d9 . u) by A29, YELLOW_0:1;
 g9 . (d9 . u) <= g9 . x by A51, A55, ORDERS_3:def_5;
then A57: u <= g9 . x by A56, ORDERS_2:3;
 g9 . x in g9 .: D9 by A49, FUNCT_2:35;
then  g9 . x <= sup (g9 .: D9) by YELLOW_2:22;
then A58: u <= sup (g9 .: D9) by A57, ORDERS_2:3;
 (downarrow (sup (g9 .: D9))) ` is upper by A33, WAYBEL11:def_4;
then  sup (g9 .: D9) in (downarrow (sup (g9 .: D9))) ` by A54, A58, WAYBEL_0:def_20;
hence  contradiction by A29, A46, YELLOW_0:17, YELLOW_0:26; ::_thesis: verum
end;
hence  "\/" ((g .: D),T) = g . ("\/" (D,S)) by A32, ORDERS_2:2; ::_thesis: verum
end;

definition
let S, T be non empty reflexive RelStr ;
let f be Function of S,T;
attrf is waybelow-preserving  means :Def8: :: WAYBEL34:def 8
 for x, y being Element of S st x << y holds
f . x << f . y;
end;

:: deftheorem Def8 defines waybelow-preserving WAYBEL34:def_8_:_
 for S, T being non empty reflexive RelStr
for f being Function of S,T holds
( f is waybelow-preserving iff for x, y being Element of S st x << y holds
f . x << f . y );

theorem Th22: :: WAYBEL34:22
for S, T being complete LATTICE
for g being infs-preserving Function of S,T st g is directed-sups-preserving holds
LowerAdj g is waybelow-preserving
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T st g is directed-sups-preserving holds
LowerAdj g is waybelow-preserving
let g be infs-preserving Function of S,T; ::_thesis: ( g is directed-sups-preserving implies LowerAdj g is waybelow-preserving )
assume A1: g is directed-sups-preserving ; ::_thesis: LowerAdj g is waybelow-preserving
set d = LowerAdj g;
A2: [g,(LowerAdj g)] is Galois by Def1;
let t, t9 be Element of T; :: according to WAYBEL34:def_8 ::_thesis: ( t << t9 implies (LowerAdj g) . t << (LowerAdj g) . t9 )
assume A3: t << t9 ; ::_thesis: (LowerAdj g) . t << (LowerAdj g) . t9
let D be non empty directed Subset of S; :: according to WAYBEL_3:def_1 ::_thesis: ( not (LowerAdj g) . t9 <= "\/" (D,S) or ex b1 being Element of the carrier of S st
( b1 in D & (LowerAdj g) . t <= b1 ) )
assume  (LowerAdj g) . t9 <= sup D ; ::_thesis: ex b1 being Element of the carrier of S st
( b1 in D & (LowerAdj g) . t <= b1 )
then A4: t9 <= g . (sup D) by A2, WAYBEL_1:8;
A5: g preserves_sup_of D by A1, WAYBEL_0:def_37;
 ex_sup_of D,S by YELLOW_0:17;
then A6: g . (sup D) = sup (g .: D) by A5, WAYBEL_0:def_31;
 ( g .: D is directed & not g .: D is empty ) by YELLOW_2:15;
then consider x being Element of T such that
A7: x in g .: D and
A8: t <= x by A3, A4, A6, WAYBEL_3:def_1;
consider s being set  such that
A9: s in the carrier of S and
A10: s in D and
A11: x = g . s by A7, FUNCT_2:64;
reconsider s = s as Element of S by A9;
take  s ; ::_thesis: ( s in D & (LowerAdj g) . t <= s )
thus  ( s in D & (LowerAdj g) . t <= s ) by A2, A8, A10, A11, WAYBEL_1:8; ::_thesis: verum
end;

theorem Th23: :: WAYBEL34:23
for S being complete LATTICE
for T being continuous complete LATTICE
for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds
g is directed-sups-preserving
proof
let S be complete LATTICE; ::_thesis: for T being continuous complete LATTICE
for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds
g is directed-sups-preserving
let T be continuous complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds
g is directed-sups-preserving
let g be infs-preserving Function of S,T; ::_thesis: ( LowerAdj g is waybelow-preserving implies g is directed-sups-preserving )
assume A1: for t, t9 being Element of T st t << t9 holds
(LowerAdj g) . t << (LowerAdj g) . t9 ; :: according to WAYBEL34:def_8 ::_thesis: g is directed-sups-preserving
let D be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or g preserves_sup_of D )
assume A2: ( not D is empty & D is directed ) ; ::_thesis: g preserves_sup_of D
assume  ex_sup_of D,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: D,T & "\/" ((g .: D),T) = g . ("\/" (D,S)) )
thus  ex_sup_of g .: D,T by YELLOW_0:17; ::_thesis: "\/" ((g .: D),T) = g . ("\/" (D,S))
A3: sup (g .: D) <= g . (sup D) by WAYBEL17:15;
A4: g . (sup D) = sup (waybelow (g . (sup D))) by WAYBEL_3:def_5;
 waybelow (g . (sup D)) is_<=_than sup (g .: D)
proof
let t be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not t in waybelow (g . (sup D)) or t <= sup (g .: D) )
assume  t in waybelow (g . (sup D)) ; ::_thesis: t <= sup (g .: D)
then  t << g . (sup D) by WAYBEL_3:7;
then A5: (LowerAdj g) . t << (LowerAdj g) . (g . (sup D)) by A1;
A6: [g,(LowerAdj g)] is Galois by Def1;
then A7: (LowerAdj g) * g <= id S by WAYBEL_1:18;
 (id S) . (sup D) = sup D by FUNCT_1:18;
then  ((LowerAdj g) * g) . (sup D) <= sup D by A7, YELLOW_2:9;
then  (LowerAdj g) . (g . (sup D)) <= sup D by FUNCT_2:15;
then consider x being Element of S such that
A8: x in D and
A9: (LowerAdj g) . t <= x by A2, A5, WAYBEL_3:def_1;
A10: g . x in g .: D by A8, FUNCT_2:35;
A11: t <= g . x by A6, A9, WAYBEL_1:8;
 g . x <= sup (g .: D) by A10, YELLOW_2:22;
hence  t <= sup (g .: D) by A11, ORDERS_2:3; ::_thesis: verum
end;
then  g . (sup D) <= sup (g .: D) by A4, YELLOW_0:32;
hence  "\/" ((g .: D),T) = g . ("\/" (D,S)) by A3, ORDERS_2:2; ::_thesis: verum
end;

definition
let S, T be TopSpace;
let f be Function of S,T;
attrf is relatively_open  means :Def9: :: WAYBEL34:def 9
 for V being open Subset of S holds f .: V is open Subset of (T | (rng f));
end;

:: deftheorem Def9 defines relatively_open WAYBEL34:def_9_:_
 for S, T being TopSpace
for f being Function of S,T holds
( f is relatively_open iff for V being open Subset of S holds f .: V is open Subset of (T | (rng f)) );

theorem :: WAYBEL34:24
for X, Y being non empty TopSpace
for d being Function of X,Y holds
( d is relatively_open iff corestr d is open )
proof
let X, Y be non empty TopSpace; ::_thesis: for d being Function of X,Y holds
( d is relatively_open iff corestr d is open )
let d be Function of X,Y; ::_thesis: ( d is relatively_open iff corestr d is open )
A1: corestr d = d by WAYBEL18:def_7;
A2: Image d = Y | (rng d) by WAYBEL18:def_6;
thus  ( d is relatively_open implies corestr d is open ) ::_thesis: ( corestr d is open implies d is relatively_open )
proof
assume A3: for V being open Subset of X holds d .: V is open Subset of (Y | (rng d)) ; :: according to WAYBEL34:def_9 ::_thesis: corestr d is open
let V be Subset of X; :: according to T_0TOPSP:def_2 ::_thesis: ( not V is open or (corestr d) .: V is open )
assume  V is open ; ::_thesis: (corestr d) .: V is open
hence  (corestr d) .: V is open by A1, A2, A3; ::_thesis: verum
end;
assume A4: for V being Subset of X st V is open holds
(corestr d) .: V is open ; :: according to T_0TOPSP:def_2 ::_thesis: d is relatively_open
let V be open Subset of X; :: according to WAYBEL34:def_9 ::_thesis: d .: V is open Subset of (Y | (rng d))
thus  d .: V is open Subset of (Y | (rng d)) by A1, A2, A4; ::_thesis: verum
end;

theorem Th25: :: WAYBEL34:25
for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
let g be infs-preserving Function of S,T; ::_thesis: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
let X be Scott TopAugmentation of T; ::_thesis: for Y being Scott TopAugmentation of S
for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
let Y be Scott TopAugmentation of S; ::_thesis: for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
A1: RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A2: RelStr(# the carrier of Y, the InternalRel of Y #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then reconsider d = LowerAdj g as Function of X,Y by A1;
let V be open Subset of X; ::_thesis: (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
reconsider A = uparrow ((LowerAdj g) .: V) as Subset of Y by A2;
 d .: V = A /\ (rng d)
proof
A3: d .: V c= A by WAYBEL_0:16;
 d .: V c= rng d by RELAT_1:111;
hence  d .: V c= A /\ (rng d) by A3, XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: A /\ (rng d) c= d .: V
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in A /\ (rng d) or t in d .: V )
assume A4: t in A /\ (rng d) ; ::_thesis: t in d .: V
then A5: t in A by XBOOLE_0:def_4;
A6: t in rng d by A4, XBOOLE_0:def_4;
reconsider t = t as Element of S by A5;
consider x being Element of S such that
A7: x <= t and
A8: x in (LowerAdj g) .: V by A5, WAYBEL_0:def_16;
consider u being set  such that
A9: u in the carrier of T and
A10: u in V and
A11: x = (LowerAdj g) . u by A8, FUNCT_2:64;
 dom d = the carrier of T by FUNCT_2:def_1;
then consider v being set  such that
A12: v in the carrier of T and
A13: t = d . v by A6, FUNCT_1:def_3;
reconsider u = u, v = v as Element of T by A9, A12;
A14: (LowerAdj g) . (u "\/" v) = x "\/" t by A11, A13, WAYBEL_6:2
.= t by A7, YELLOW_0:24 ;
reconsider V9 = V as Subset of T by A1;
 V is upper by WAYBEL11:def_4;
then A15: V9 is upper by A1, WAYBEL_0:25;
 u <= u "\/" v by YELLOW_0:22;
then  u "\/" v in V9 by A10, A15, WAYBEL_0:def_20;
hence  t in d .: V by A14, FUNCT_2:35; ::_thesis: verum
end;
hence  (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V)) ; ::_thesis: verum
end;

theorem Th26: :: WAYBEL34:26
for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S st ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) holds
for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S st ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) holds
for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
let g be infs-preserving Function of S,T; ::_thesis: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S st ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) holds
for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
let X be Scott TopAugmentation of T; ::_thesis: for Y being Scott TopAugmentation of S st ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) holds
for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
let Y be Scott TopAugmentation of S; ::_thesis: ( ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) implies for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open )
assume A1: for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ; ::_thesis: for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
let d be Function of X,Y; ::_thesis: ( d = LowerAdj g implies d is relatively_open )
assume A2: d = LowerAdj g ; ::_thesis: d is relatively_open
let V be open Subset of X; :: according to WAYBEL34:def_9 ::_thesis: d .: V is open Subset of (Y | (rng d))
reconsider A = uparrow ((LowerAdj g) .: V) as open Subset of Y by A1;
 d .: V = A /\ (rng d) by A2, Th25;
then A3: d .: V = ([#] (Y | (rng d))) /\ A by PRE_TOPC:def_5;
A4: A in the topology of Y by PRE_TOPC:def_2;
reconsider B = d .: V as Subset of (Y | (rng d)) by A3, XBOOLE_1:17;
 B in the topology of (Y | (rng d)) by A3, A4, PRE_TOPC:def_4;
hence  d .: V is open Subset of (Y | (rng d)) by PRE_TOPC:def_2; ::_thesis: verum
end;

registration
let X, Y be complete LATTICE;
let f be sups-preserving Function of X,Y;
cluster Image f ->  complete ;
coherence
 Image f is complete by YELLOW_2:34;
end;

theorem :: WAYBEL34:27
for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds
d9 is open
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds
d9 is open
let g be infs-preserving Function of S,T; ::_thesis: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds
d9 is open
let X be Scott TopAugmentation of T; ::_thesis: for Y being Scott TopAugmentation of S
for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds
d9 is open
let Y be Scott TopAugmentation of S; ::_thesis: for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds
d9 is open
let Z be Scott TopAugmentation of Image (LowerAdj g); ::_thesis: for d being Function of X,Y
for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds
d9 is open
let d be Function of X,Y; ::_thesis: for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds
d9 is open
let d9 be Function of X,Z; ::_thesis: ( d = LowerAdj g & d9 = d & d is relatively_open implies d9 is open )
assume that
A1: d = LowerAdj g and
A2: d9 = d and
A3: for V being open Subset of X holds d .: V is open Subset of (Y | (rng d)) ; :: according to WAYBEL34:def_9 ::_thesis: d9 is open
let V be Subset of X; :: according to T_0TOPSP:def_2 ::_thesis: ( not V is open or d9 .: V is open )
assume  V is open ; ::_thesis: d9 .: V is open
then reconsider A = d .: V as open Subset of (Y | (rng d)) by A3;
A4: Image (LowerAdj g) = subrelstr (rng (LowerAdj g)) by YELLOW_2:def_2;
then A5: the carrier of (Image (LowerAdj g)) = rng d by A1, YELLOW_0:def_15;
A6: [#] (Y | (rng d)) = rng d by PRE_TOPC:def_5;
A7: RelStr(# the carrier of Z, the InternalRel of Z #) = Image (LowerAdj g) by YELLOW_9:def_4;
A8: RelStr(# the carrier of Y, the InternalRel of Y #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
reconsider B = A as Subset of Z by A1, A4, A6, A7, YELLOW_0:def_15;
 A in the topology of (Y | (rng d)) by PRE_TOPC:def_2;
then consider C being Subset of Y such that
A9: C in the topology of Y and
A10: A = C /\ ([#] (Y | (rng d))) by PRE_TOPC:def_4;
 C is open by A9, PRE_TOPC:def_2;
then A11: ( C is upper & C is inaccessible ) by WAYBEL11:def_4;
A12: B is upper
proof
let x, y be Element of Z; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in B or not x <= y or y in B )
reconsider x9 = x, y9 = y as Element of (Image (LowerAdj g)) by A7;
reconsider a = x9, b = y9 as Element of S by YELLOW_0:58;
reconsider a9 = a, b9 = b as Element of Y by A8;
assume that
A13: x in B and
A14: x <= y ; ::_thesis: y in B
A15: x9 <= y9 by A7, A14, YELLOW_0:1;
A16: a in C by A10, A13, XBOOLE_0:def_4;
 a <= b by A15, YELLOW_0:59;
then  a9 <= b9 by A8, YELLOW_0:1;
then  b9 in C by A11, A16, WAYBEL_0:def_20;
hence  y in B by A5, A6, A10, XBOOLE_0:def_4; ::_thesis: verum
end;
 B is inaccessible
proof
let D be non empty directed Subset of Z; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,Z) in B or not D misses B )
assume A17: sup D in B ; ::_thesis: not D misses B
reconsider D9 = D as non empty Subset of (Image (LowerAdj g)) by A7;
reconsider E = D9 as non empty Subset of S by A5, A8, XBOOLE_1:1;
reconsider E9 = E as non empty Subset of Y by A8;
 D9 is directed by A7, WAYBEL_0:3;
then  E is directed by YELLOW_2:7;
then A18: E9 is directed by A8, WAYBEL_0:3;
A19: ex_sup_of D9,S by YELLOW_0:17;
 Image (LowerAdj g) is sups-inheriting by YELLOW_2:32;
then  "\/" (D9,S) in the carrier of (Image (LowerAdj g)) by A19, YELLOW_0:def_19;
then  sup E = sup D9 by YELLOW_0:68
.= sup D by A7, YELLOW_0:17, YELLOW_0:26 ;
then  sup E9 = sup D by A8, YELLOW_0:17, YELLOW_0:26;
then  sup E9 in C by A10, A17, XBOOLE_0:def_4;
then  C meets E by A11, A18, WAYBEL11:def_1;
hence  not D misses B by A5, A6, A10, XBOOLE_1:77; ::_thesis: verum
end;
hence  d9 .: V is open by A2, A12, WAYBEL11:def_4; ::_thesis: verum
end;

theorem Th28: :: WAYBEL34:28
for S, T being complete LATTICE
for g being infs-preserving Function of S,T st g is V7() holds
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
proof
let S, T be complete LATTICE; ::_thesis: for g being infs-preserving Function of S,T st g is V7() holds
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let g be infs-preserving Function of S,T; ::_thesis: ( g is V7() implies for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open ) )
assume A1: g is V7() ; ::_thesis: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let X be Scott TopAugmentation of T; ::_thesis: for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let Y be Scott TopAugmentation of S; ::_thesis: for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
 [g,(LowerAdj g)] is Galois by Def1;
then  LowerAdj g is onto by A1, WAYBEL_1:27;
then A2: rng (LowerAdj g) = the carrier of S by FUNCT_2:def_3;
A3: RelStr(# the carrier of Y, the InternalRel of Y #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
A4: RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A5: [#] Y = the carrier of Y ;
let d be Function of X,Y; ::_thesis: ( d = LowerAdj g implies ( g is directed-sups-preserving iff d is open ) )
assume A6: d = LowerAdj g ; ::_thesis: ( g is directed-sups-preserving iff d is open )
A7: Y | (rng d) = TopStruct(# the carrier of Y, the topology of Y #) by A2, A3, A5, A6, TSEP_1:93;
thus  ( g is directed-sups-preserving implies d is open ) ::_thesis: ( d is open implies g is directed-sups-preserving )
proof
assume  g is directed-sups-preserving ; ::_thesis: d is open
then  for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y by Th21;
then A8: d is relatively_open by A6, Th26;
let V be Subset of X; :: according to T_0TOPSP:def_2 ::_thesis: ( not V is open or d .: V is open )
assume  V is open ; ::_thesis: d .: V is open
then  d .: V is open Subset of (Y | (rng d)) by A8, Def9;
hence  d .: V in the topology of Y by A7, PRE_TOPC:def_2; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
assume A9: for V being Subset of X st V is open holds
d .: V is open ; :: according to T_0TOPSP:def_2 ::_thesis: g is directed-sups-preserving
now__::_thesis:_for_X9_being_Scott_TopAugmentation_of_T
for_Y9_being_Scott_TopAugmentation_of_S
for_V9_being_open_Subset_of_X9_holds_uparrow_((LowerAdj_g)_.:_V9)_is_open_Subset_of_Y9
let X9 be Scott TopAugmentation of T; ::_thesis: for Y9 being Scott TopAugmentation of S
for V9 being open Subset of X9 holds uparrow ((LowerAdj g) .: V9) is open Subset of Y9
let Y9 be Scott TopAugmentation of S; ::_thesis: for V9 being open Subset of X9 holds uparrow ((LowerAdj g) .: V9) is open Subset of Y9
let V9 be open Subset of X9; ::_thesis: uparrow ((LowerAdj g) .: V9) is open Subset of Y9
A10: RelStr(# the carrier of X9, the InternalRel of X9 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A11: RelStr(# the carrier of Y9, the InternalRel of Y9 #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
reconsider V = V9 as Subset of X by A4, A10;
reconsider V = V as open Subset of X by A4, A10, YELLOW_9:50;
reconsider d9 = d as Function of X9,Y9 by A3, A4, A10, A11;
 d .: V is open by A9;
then A12: d9 .: V9 is open Subset of Y9 by A3, A11, YELLOW_9:50;
then  d9 .: V9 is upper by WAYBEL11:def_4;
then A13: uparrow (d9 .: V9) c= d9 .: V9 by WAYBEL_0:24;
 d9 .: V9 c= uparrow (d9 .: V9) by WAYBEL_0:16;
then  uparrow (d9 .: V9) = d9 .: V9 by A13, XBOOLE_0:def_10;
hence  uparrow ((LowerAdj g) .: V9) is open Subset of Y9 by A6, A11, A12, WAYBEL_0:13; ::_thesis: verum
end;
hence  g is directed-sups-preserving by Th21; ::_thesis: verum
end;

registration
let X be complete LATTICE;
let f be projection Function of X,X;
cluster Image f ->  complete ;
coherence
 Image f is complete by WAYBEL_1:54;
end;

theorem Th29: :: WAYBEL34:29
for L being complete LATTICE
for k being kernel Function of L,L holds
( corestr k is infs-preserving & inclusion k is sups-preserving & LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k )
proof
let L be complete LATTICE; ::_thesis: for k being kernel Function of L,L holds
( corestr k is infs-preserving & inclusion k is sups-preserving & LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k )
let k be kernel Function of L,L; ::_thesis: ( corestr k is infs-preserving & inclusion k is sups-preserving & LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k )
A1: [(corestr k),(inclusion k)] is Galois by WAYBEL_1:39;
then A2: inclusion k is lower_adjoint by WAYBEL_1:def_12;
A3: corestr k is upper_adjoint by A1, WAYBEL_1:def_11;
hence  ( corestr k is infs-preserving & inclusion k is sups-preserving ) by A2; ::_thesis: ( LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k )
thus  ( LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k ) by A1, A2, A3, Def1, Def2; ::_thesis: verum
end;

theorem Th30: :: WAYBEL34:30
for L being complete LATTICE
for k being kernel Function of L,L holds
( k is directed-sups-preserving iff corestr k is directed-sups-preserving )
proof
let L be complete LATTICE; ::_thesis: for k being kernel Function of L,L holds
( k is directed-sups-preserving iff corestr k is directed-sups-preserving )
let k be kernel Function of L,L; ::_thesis: ( k is directed-sups-preserving iff corestr k is directed-sups-preserving )
set ck = corestr k;
 [(corestr k),(inclusion k)] is Galois by WAYBEL_1:39;
then A1: inclusion k is lower_adjoint by WAYBEL_1:def_12;
A2: k = (inclusion k) * (corestr k) by WAYBEL_1:32;
hereby  ::_thesis: ( corestr k is directed-sups-preserving implies k is directed-sups-preserving )
assume A3: k is directed-sups-preserving ; ::_thesis: corestr k is directed-sups-preserving
thus  corestr k is directed-sups-preserving ::_thesis: verum
proof
let D be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or corestr k preserves_sup_of D )
assume  ( not D is empty & D is directed ) ; ::_thesis: corestr k preserves_sup_of D
then A4: k preserves_sup_of D by A3, WAYBEL_0:def_37;
assume  ex_sup_of D,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (corestr k) .: D, Image k & "\/" (((corestr k) .: D),(Image k)) = (corestr k) . ("\/" (D,L)) )
then A5: sup (k .: D) = k . (sup D) by A4, WAYBEL_0:def_31
.= (inclusion k) . ((corestr k) . (sup D)) by A2, FUNCT_2:15
.= (corestr k) . (sup D) by FUNCT_1:18 ;
thus  ex_sup_of (corestr k) .: D, Image k by YELLOW_0:17; ::_thesis: "\/" (((corestr k) .: D),(Image k)) = (corestr k) . ("\/" (D,L))
A6: ex_sup_of (inclusion k) .: ((corestr k) .: D),L by YELLOW_0:17;
A7: Image k is sups-inheriting by WAYBEL_1:53;
 ex_sup_of (corestr k) .: D,L by YELLOW_0:17;
then A8: "\/" (((corestr k) .: D),L) in the carrier of (Image k) by A7, YELLOW_0:def_19;
 (corestr k) .: D = (inclusion k) .: ((corestr k) .: D) by WAYBEL15:12;
hence  sup ((corestr k) .: D) = sup ((inclusion k) .: ((corestr k) .: D)) by A6, A8, YELLOW_0:64
.= (corestr k) . (sup D) by A2, A5, RELAT_1:126 ;
::_thesis: verum
end;
end;
thus  ( corestr k is directed-sups-preserving implies k is directed-sups-preserving ) by A1, A2, WAYBEL15:11; ::_thesis: verum
end;

theorem :: WAYBEL34:31
for L being complete LATTICE
for k being kernel Function of L,L holds
( k is directed-sups-preserving iff for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y )
proof
let L be complete LATTICE; ::_thesis: for k being kernel Function of L,L holds
( k is directed-sups-preserving iff for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y )
let k be kernel Function of L,L; ::_thesis: ( k is directed-sups-preserving iff for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y )
A1: [(corestr k),(inclusion k)] is Galois by WAYBEL_1:39;
then A2: corestr k is upper_adjoint by WAYBEL_1:def_11;
then A3: inclusion k = LowerAdj (corestr k) by A1, Def1;
hereby  ::_thesis: ( ( for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y ) implies k is directed-sups-preserving )
assume A4: k is directed-sups-preserving ; ::_thesis: for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y
let X be Scott TopAugmentation of Image k; ::_thesis: for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y
let Y be Scott TopAugmentation of L; ::_thesis: for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y
A5: RelStr(# the carrier of X, the InternalRel of X #) = Image k by YELLOW_9:def_4;
let V be Subset of L; ::_thesis: ( V is open Subset of X implies uparrow V is open Subset of Y )
assume  V is open Subset of X ; ::_thesis: uparrow V is open Subset of Y
then reconsider A = V as open Subset of X ;
reconsider B = A as Subset of (Image k) by A5;
A6: corestr k is directed-sups-preserving by A4, Th30;
 (inclusion k) .: B = V by WAYBEL15:12;
hence  uparrow V is open Subset of Y by A2, A3, A6, Th21; ::_thesis: verum
end;
assume A7: for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y ; ::_thesis: k is directed-sups-preserving
now__::_thesis:_for_X_being_Scott_TopAugmentation_of_Image_k
for_Y_being_Scott_TopAugmentation_of_L
for_V_being_open_Subset_of_X_holds_uparrow_((LowerAdj_(corestr_k))_.:_V)_is_open_Subset_of_Y
set g = corestr k;
let X be Scott TopAugmentation of Image k; ::_thesis: for Y being Scott TopAugmentation of L
for V being open Subset of X holds uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y
let Y be Scott TopAugmentation of L; ::_thesis: for V being open Subset of X holds uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y
let V be open Subset of X; ::_thesis: uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y
 RelStr(# the carrier of X, the InternalRel of X #) = Image k by YELLOW_9:def_4;
then reconsider B = V as Subset of (Image k) ;
 the carrier of (Image k) c= the carrier of L by YELLOW_0:def_13;
then reconsider A = B as Subset of L by XBOOLE_1:1;
 uparrow A is open Subset of Y by A7;
hence  uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y by A3, WAYBEL15:12; ::_thesis: verum
end;
then  corestr k is directed-sups-preserving by A2, Th21;
hence  k is directed-sups-preserving by Th30; ::_thesis: verum
end;

theorem Th32: :: WAYBEL34:32
for L being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of L
for x, y being Element of L
for a, b being Element of S st a = x & b = y & x << y holds
a << b
proof
let L be complete LATTICE; ::_thesis: for S being non empty full sups-inheriting SubRelStr of L
for x, y being Element of L
for a, b being Element of S st a = x & b = y & x << y holds
a << b
let S be non empty full sups-inheriting SubRelStr of L; ::_thesis: for x, y being Element of L
for a, b being Element of S st a = x & b = y & x << y holds
a << b
let x, y be Element of L; ::_thesis: for a, b being Element of S st a = x & b = y & x << y holds
a << b
let a, b be Element of S; ::_thesis: ( a = x & b = y & x << y implies a << b )
assume that
A1: a = x and
A2: b = y and
A3: for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d ) ; :: according to WAYBEL_3:def_1 ::_thesis: a << b
let D be non empty directed Subset of S; :: according to WAYBEL_3:def_1 ::_thesis: ( not b <= "\/" (D,S) or ex b1 being Element of the carrier of S st
( b1 in D & a <= b1 ) )
assume A4: b <= sup D ; ::_thesis: ex b1 being Element of the carrier of S st
( b1 in D & a <= b1 )
reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A5: ex_sup_of D,L by YELLOW_0:17;
then  "\/" (D,L) in the carrier of S by YELLOW_0:def_19;
then  sup E = sup D by A5, YELLOW_0:64;
then  y <= sup E by A2, A4, YELLOW_0:59;
then consider e being Element of L such that
A6: e in E and
A7: x <= e by A3;
reconsider d = e as Element of S by A6;
take  d ; ::_thesis: ( d in D & a <= d )
thus  ( d in D & a <= d ) by A1, A6, A7, YELLOW_0:60; ::_thesis: verum
end;

theorem :: WAYBEL34:33
for L being complete LATTICE
for k being kernel Function of L,L st k is directed-sups-preserving holds
for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b )
proof
let L be complete LATTICE; ::_thesis: for k being kernel Function of L,L st k is directed-sups-preserving holds
for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b )
let k be kernel Function of L,L; ::_thesis: ( k is directed-sups-preserving implies for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b ) )
set g = corestr k;
assume  k is directed-sups-preserving ; ::_thesis: for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b )
then  ( corestr k is directed-sups-preserving & corestr k is infs-preserving ) by Th29, Th30;
then A1: LowerAdj (corestr k) is waybelow-preserving by Th22;
let x, y be Element of L; ::_thesis: for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b )
let a, b be Element of (Image k); ::_thesis: ( a = x & b = y implies ( x << y iff a << b ) )
A2: Image k is sups-inheriting by WAYBEL_1:53;
A3: inclusion k = LowerAdj (corestr k) by Th29;
then A4: (LowerAdj (corestr k)) . a = a by FUNCT_1:18;
 (LowerAdj (corestr k)) . b = b by A3, FUNCT_1:18;
hence  ( a = x & b = y implies ( x << y iff a << b ) ) by A1, A2, A4, Def8, Th32; ::_thesis: verum
end;

theorem :: WAYBEL34:34
for L being complete LATTICE
for k being kernel Function of L,L st Image k is continuous & ( for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b ) ) holds
k is directed-sups-preserving
proof
let L be complete LATTICE; ::_thesis: for k being kernel Function of L,L st Image k is continuous & ( for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b ) ) holds
k is directed-sups-preserving
let k be kernel Function of L,L; ::_thesis: ( Image k is continuous & ( for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b ) ) implies k is directed-sups-preserving )
assume that
A1: Image k is continuous and
A2: for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b ) ; ::_thesis: k is directed-sups-preserving
set g = corestr k;
A3: corestr k is infs-preserving by Th29;
 LowerAdj (corestr k) is waybelow-preserving
proof
let t, t9 be Element of (Image k); :: according to WAYBEL34:def_8 ::_thesis: ( t << t9 implies (LowerAdj (corestr k)) . t << (LowerAdj (corestr k)) . t9 )
A4: LowerAdj (corestr k) = inclusion k by Th29;
then A5: (LowerAdj (corestr k)) . t = t by FUNCT_1:18;
 (LowerAdj (corestr k)) . t9 = t9 by A4, FUNCT_1:18;
hence  ( t << t9 implies (LowerAdj (corestr k)) . t << (LowerAdj (corestr k)) . t9 ) by A2, A5; ::_thesis: verum
end;
then  corestr k is directed-sups-preserving by A1, A3, Th23;
hence  k is directed-sups-preserving by Th30; ::_thesis: verum
end;

theorem Th35: :: WAYBEL34:35
for L being complete LATTICE
for c being closure Function of L,L holds
( corestr c is sups-preserving & inclusion c is infs-preserving & UpperAdj (corestr c) = inclusion c & LowerAdj (inclusion c) = corestr c )
proof
let L be complete LATTICE; ::_thesis: for c being closure Function of L,L holds
( corestr c is sups-preserving & inclusion c is infs-preserving & UpperAdj (corestr c) = inclusion c & LowerAdj (inclusion c) = corestr c )
let c be closure Function of L,L; ::_thesis: ( corestr c is sups-preserving & inclusion c is infs-preserving & UpperAdj (corestr c) = inclusion c & LowerAdj (inclusion c) = corestr c )
A1: [(inclusion c),(corestr c)] is Galois by WAYBEL_1:36;
then A2: inclusion c is upper_adjoint by WAYBEL_1:def_11;
A3: corestr c is lower_adjoint by A1, WAYBEL_1:def_12;
hence  ( corestr c is sups-preserving & inclusion c is infs-preserving ) by A2; ::_thesis: ( UpperAdj (corestr c) = inclusion c & LowerAdj (inclusion c) = corestr c )
thus  ( UpperAdj (corestr c) = inclusion c & LowerAdj (inclusion c) = corestr c ) by A1, A2, A3, Def1, Def2; ::_thesis: verum
end;

theorem Th36: :: WAYBEL34:36
for L being complete LATTICE
for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving )
proof
let L be complete LATTICE; ::_thesis: for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving )
let c be closure Function of L,L; ::_thesis: ( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving )
set ic = inclusion c;
thus  ( Image c is directed-sups-inheriting implies inclusion c is directed-sups-preserving ) ::_thesis: ( inclusion c is directed-sups-preserving implies Image c is directed-sups-inheriting )
proof
assume A1: Image c is directed-sups-inheriting ; ::_thesis: inclusion c is directed-sups-preserving
let D be Subset of (Image c); :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or inclusion c preserves_sup_of D )
assume A2: ( not D is empty & D is directed ) ; ::_thesis: inclusion c preserves_sup_of D
then reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A3: (inclusion c) .: D = E by WAYBEL15:12;
assume  ex_sup_of D, Image c ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (inclusion c) .: D,L & "\/" (((inclusion c) .: D),L) = (inclusion c) . ("\/" (D,(Image c))) )
thus  ex_sup_of (inclusion c) .: D,L by YELLOW_0:17; ::_thesis: "\/" (((inclusion c) .: D),L) = (inclusion c) . ("\/" (D,(Image c)))
hence  sup ((inclusion c) .: D) = sup D by A1, A2, A3, WAYBEL_0:7
.= (inclusion c) . (sup D) by FUNCT_1:18 ;
::_thesis: verum
end;
assume A4: inclusion c is directed-sups-preserving ; ::_thesis: Image c is directed-sups-inheriting
let X be directed Subset of (Image c); :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image c) )
assume A5: X <> {} ; ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image c) )
assume  ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (Image c)
A6: inclusion c preserves_sup_of X by A4, A5, WAYBEL_0:def_37;
 ex_sup_of X, Image c by YELLOW_0:17;
then  sup ((inclusion c) .: X) = (inclusion c) . (sup X) by A6, WAYBEL_0:def_31
.= sup X by FUNCT_1:18 ;
then  sup ((inclusion c) .: X) in the carrier of (Image c) ;
hence  "\/" (X,L) in the carrier of (Image c) by WAYBEL15:12; ::_thesis: verum
end;

theorem :: WAYBEL34:37
for L being complete LATTICE
for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open )
proof
let L be complete LATTICE; ::_thesis: for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open )
let c be closure Function of L,L; ::_thesis: ( Image c is directed-sups-inheriting iff for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open )
A1: LowerAdj (inclusion c) = corestr c by Th35;
A2: corestr c = c by WAYBEL_1:30;
A3: inclusion c is infs-preserving Function of (Image c),L by Th35;
A4: ( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving ) by Th36;
hence  ( Image c is directed-sups-inheriting implies for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open ) by A1, A2, A3, Th28; ::_thesis: ( ( for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open ) implies Image c is directed-sups-inheriting )
assume A5: for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open ; ::_thesis: Image c is directed-sups-inheriting
set X = the Scott TopAugmentation of Image c;
set Y = the Scott TopAugmentation of L;
A6: RelStr(# the carrier of the Scott TopAugmentation of Image c, the InternalRel of the Scott TopAugmentation of Image c #) = RelStr(# the carrier of (Image c), the InternalRel of (Image c) #) by YELLOW_9:def_4;
 RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4;
then reconsider f = c as Function of the Scott TopAugmentation of L, the Scott TopAugmentation of Image c by A2, A6;
 f is open by A5;
hence  Image c is directed-sups-inheriting by A1, A2, A3, A4, Th28; ::_thesis: verum
end;

theorem :: WAYBEL34:38
for L being complete LATTICE
for c being closure Function of L,L st Image c is directed-sups-inheriting holds
corestr c is waybelow-preserving
proof
let L be complete LATTICE; ::_thesis: for c being closure Function of L,L st Image c is directed-sups-inheriting holds
corestr c is waybelow-preserving
let c be closure Function of L,L; ::_thesis: ( Image c is directed-sups-inheriting implies corestr c is waybelow-preserving )
assume  Image c is directed-sups-inheriting ; ::_thesis: corestr c is waybelow-preserving
then  ( inclusion c is directed-sups-preserving & inclusion c is infs-preserving ) by Th35, Th36;
then  LowerAdj (inclusion c) is waybelow-preserving by Th22;
hence  corestr c is waybelow-preserving by Th35; ::_thesis: verum
end;

theorem :: WAYBEL34:39
for L being continuous complete LATTICE
for c being closure Function of L,L st corestr c is waybelow-preserving holds
Image c is directed-sups-inheriting
proof
let L be continuous complete LATTICE; ::_thesis: for c being closure Function of L,L st corestr c is waybelow-preserving holds
Image c is directed-sups-inheriting
let c be closure Function of L,L; ::_thesis: ( corestr c is waybelow-preserving implies Image c is directed-sups-inheriting )
assume A1: corestr c is waybelow-preserving ; ::_thesis: Image c is directed-sups-inheriting
A2: LowerAdj (inclusion c) = corestr c by Th35;
 inclusion c is infs-preserving by Th35;
then  inclusion c is directed-sups-preserving by A1, A2, Th23;
hence  Image c is directed-sups-inheriting by Th36; ::_thesis: verum
end;

begin

definition
let W be non empty set ;
set A = W -INF_category ;
defpred S1[ set ] means verum;
defpred S2[ object of (W -INF_category), object of (W -INF_category), Morphism of $1,$2] means  @ $3 is directed-sups-preserving ;
A1: ex a being object of (W -INF_category) st S1[a] ;
A2: for a, b, c being object of (W -INF_category) st S1[a] & S1[b] & S1[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
proof
let a, b, c be object of (W -INF_category); ::_thesis: ( S1[a] & S1[b] & S1[c] & <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f] )
assume that
A3: <^a,b^> <> {} and
A4: <^b,c^> <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
let g be Morphism of b,c; ::_thesis: ( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
A5: <^a,c^> <> {} by A3, A4, ALTCAT_1:def_2;
A6: @ f = f by A3, YELLOW21:def_7;
A7: @ g = g by A4, YELLOW21:def_7;
 @ (g * f) = g * f by A5, YELLOW21:def_7;
then  @ (g * f) = (@ g) * (@ f) by A3, A4, A5, A6, A7, ALTCAT_1:def_12;
hence  ( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] ) by WAYBEL20:28; ::_thesis: verum
end;
A8: for a being object of (W -INF_category) st S1[a] holds
S2[a,a, idm a]
proof
let a be object of (W -INF_category); ::_thesis: ( S1[a] implies S2[a,a, idm a] )
 idm a = id (latt a) by YELLOW21:2;
hence  ( S1[a] implies S2[a,a, idm a] ) by YELLOW21:def_7; ::_thesis: verum
end;
funcW -INF(SC)_category  ->  non empty strict subcategory of W -INF_category  means :Def10: :: WAYBEL34:def 10
( ( for a being object of (W -INF_category) holds a is object of it ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of it st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) );
existence
 ex b1 being non empty strict subcategory of W -INF_category st
( ( for a being object of (W -INF_category) holds a is object of b1 ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) )
proof
 ex B being non empty strict subcategory of W -INF_category st
( ( for a being object of (W -INF_category) holds
( a is object of B iff S1[a] ) ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of B st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S2[a,b,f] ) ) ) from YELLOW18:sch_7(A1, A2, A8);
hence  ex b1 being non empty strict subcategory of W -INF_category st
( ( for a being object of (W -INF_category) holds a is object of b1 ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict subcategory of W -INF_category st ( for a being object of (W -INF_category) holds a is object of b1 ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) & ( for a being object of (W -INF_category) holds a is object of b2 ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of b2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) holds
b1 = b2;
proof
let B1, B2 be non empty strict subcategory of W -INF_category ; ::_thesis: ( ( for a being object of (W -INF_category) holds a is object of B1 ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of B1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) & ( for a being object of (W -INF_category) holds a is object of B2 ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of B2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) implies B1 = B2 )
assume  for a being object of (W -INF_category) holds a is object of B1 ; ::_thesis: ( ex a, b being object of (W -INF_category) ex a9, b9 being object of B1 st
( a9 = a & b9 = b & <^a,b^> <> {} & not  for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) or ex a being object of (W -INF_category) st a is not object of B2 or ex a, b being object of (W -INF_category) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not  for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) or B1 = B2 )
then A9: for a being object of (W -INF_category) holds
( a is object of B1 iff S1[a] ) ;
assume A10: for a, b being object of (W -INF_category)
for a9, b9 being object of B1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S2[a,b,f] ) ; ::_thesis: ( ex a being object of (W -INF_category) st a is not object of B2 or ex a, b being object of (W -INF_category) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not  for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) or B1 = B2 )
assume  for a being object of (W -INF_category) holds a is object of B2 ; ::_thesis: ( ex a, b being object of (W -INF_category) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not  for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) or B1 = B2 )
then A11: for a being object of (W -INF_category) holds
( a is object of B2 iff S1[a] ) ;
assume A12: for a, b being object of (W -INF_category)
for a9, b9 being object of B2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S2[a,b,f] ) ; ::_thesis: B1 = B2
 AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch_1(A9, A10, A11, A12);
hence  B1 = B2 ; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines -INF(SC)_category WAYBEL34:def_10_:_
 for W being non empty set
for b2 being non empty strict subcategory of W -INF_category holds
( b2 = W -INF(SC)_category iff ( ( for a being object of (W -INF_category) holds a is object of b2 ) & ( for a, b being object of (W -INF_category)
for a9, b9 being object of b2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) ) );

definition
let W be with_non-empty_element set ;
A1: ex w being non empty set st w in W by SETFAM_1:def_10;
set A = W -SUP_category ;
defpred S1[ set ] means verum;
defpred S2[ object of (W -SUP_category), object of (W -SUP_category), Morphism of $1,$2] means  UpperAdj (@ $3) is directed-sups-preserving ;
A2: ex a being object of (W -SUP_category) st S1[a] ;
A3: for a, b, c being object of (W -SUP_category) st S1[a] & S1[b] & S1[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
proof
let a, b, c be object of (W -SUP_category); ::_thesis: ( S1[a] & S1[b] & S1[c] & <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f] )
assume that
A4: <^a,b^> <> {} and
A5: <^b,c^> <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
let g be Morphism of b,c; ::_thesis: ( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
A6: <^a,c^> <> {} by A4, A5, ALTCAT_1:def_2;
A7: @ f = f by A4, YELLOW21:def_7;
A8: @ g = g by A5, YELLOW21:def_7;
A9: @ (g * f) = g * f by A6, YELLOW21:def_7;
A10: @ g is sups-preserving Function of (latt b),(latt c) by A1, A5, A8, Def5;
A11: @ f is sups-preserving Function of (latt a),(latt b) by A1, A4, A7, Def5;
 @ (g * f) = (@ g) * (@ f) by A4, A5, A6, A7, A8, A9, ALTCAT_1:def_12;
then  UpperAdj (@ (g * f)) = (UpperAdj (@ f)) * (UpperAdj (@ g)) by A10, A11, Th9;
hence  ( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] ) by WAYBEL20:28; ::_thesis: verum
end;
A12: for a being object of (W -SUP_category) st S1[a] holds
S2[a,a, idm a]
proof
let a be object of (W -SUP_category); ::_thesis: ( S1[a] implies S2[a,a, idm a] )
A13: idm a = id (latt a) by YELLOW21:2;
 UpperAdj (id (latt a)) = id (latt a) by Th7;
hence  ( S1[a] implies S2[a,a, idm a] ) by A13, YELLOW21:def_7; ::_thesis: verum
end;
funcW -SUP(SO)_category  ->  non empty strict subcategory of W -SUP_category  means :Def11: :: WAYBEL34:def 11
( ( for a being object of (W -SUP_category) holds a is object of it ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of it st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) );
existence
 ex b1 being non empty strict subcategory of W -SUP_category st
( ( for a being object of (W -SUP_category) holds a is object of b1 ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) )
proof
 ex B being non empty strict subcategory of W -SUP_category st
( ( for a being object of (W -SUP_category) holds
( a is object of B iff S1[a] ) ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of B st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S2[a,b,f] ) ) ) from YELLOW18:sch_7(A2, A3, A12);
hence  ex b1 being non empty strict subcategory of W -SUP_category st
( ( for a being object of (W -SUP_category) holds a is object of b1 ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict subcategory of W -SUP_category st ( for a being object of (W -SUP_category) holds a is object of b1 ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) & ( for a being object of (W -SUP_category) holds a is object of b2 ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) holds
b1 = b2;
proof
let B1, B2 be non empty strict subcategory of W -SUP_category ; ::_thesis: ( ( for a being object of (W -SUP_category) holds a is object of B1 ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of B1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) & ( for a being object of (W -SUP_category) holds a is object of B2 ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of B2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) implies B1 = B2 )
assume  for a being object of (W -SUP_category) holds a is object of B1 ; ::_thesis: ( ex a, b being object of (W -SUP_category) ex a9, b9 being object of B1 st
( a9 = a & b9 = b & <^a,b^> <> {} & not  for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) or ex a being object of (W -SUP_category) st a is not object of B2 or ex a, b being object of (W -SUP_category) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not  for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) or B1 = B2 )
then A14: for a being object of (W -SUP_category) holds
( a is object of B1 iff S1[a] ) ;
assume A15: for a, b being object of (W -SUP_category)
for a9, b9 being object of B1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S2[a,b,f] ) ; ::_thesis: ( ex a being object of (W -SUP_category) st a is not object of B2 or ex a, b being object of (W -SUP_category) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not  for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) or B1 = B2 )
assume  for a being object of (W -SUP_category) holds a is object of B2 ; ::_thesis: ( ex a, b being object of (W -SUP_category) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not  for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) or B1 = B2 )
then A16: for a being object of (W -SUP_category) holds
( a is object of B2 iff S1[a] ) ;
assume A17: for a, b being object of (W -SUP_category)
for a9, b9 being object of B2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S2[a,b,f] ) ; ::_thesis: B1 = B2
 AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch_1(A14, A15, A16, A17);
hence  B1 = B2 ; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines -SUP(SO)_category WAYBEL34:def_11_:_
 for W being with_non-empty_element set
for b2 being non empty strict subcategory of W -SUP_category holds
( b2 = W -SUP(SO)_category iff ( ( for a being object of (W -SUP_category) holds a is object of b2 ) & ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) ) );

theorem Th40: :: WAYBEL34:40
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr
for t being Element of T
for X being non empty Subset of S holds
( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric RelStr
for t being Element of T
for X being non empty Subset of S holds
( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
let T be non empty reflexive antisymmetric RelStr ; ::_thesis: for t being Element of T
for X being non empty Subset of S holds
( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
let t be Element of T; ::_thesis: for X being non empty Subset of S holds
( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
let X be non empty Subset of S; ::_thesis: ( S --> t preserves_sup_of X & S --> t preserves_inf_of X )
set f = S --> t;
A1: (S --> t) .: X = {t}
proof
thus  (S --> t) .: X c= {t} by FUNCOP_1:81; :: according to XBOOLE_0:def_10 ::_thesis: {t} c= (S --> t) .: X
set x = the Element of X;
 (S --> t) . the Element of X = t by FUNCOP_1:7;
then  t in (S --> t) .: X by FUNCT_2:35;
hence  {t} c= (S --> t) .: X by ZFMISC_1:31; ::_thesis: verum
end;
A2: (S --> t) . (sup X) = t by FUNCOP_1:7;
A3: (S --> t) . (inf X) = t by FUNCOP_1:7;
A4: inf {t} = t by YELLOW_0:39;
A5: sup {t} = t by YELLOW_0:39;
A6: ex_sup_of {t},T by YELLOW_0:38;
 ex_inf_of {t},T by YELLOW_0:38;
hence  ( S --> t preserves_sup_of X & S --> t preserves_inf_of X ) by A1, A2, A3, A4, A5, A6, WAYBEL_0:def_30, WAYBEL_0:def_31; ::_thesis: verum
end;

theorem Th41: :: WAYBEL34:41
for S being non empty RelStr
for T being non empty reflexive antisymmetric lower-bounded RelStr holds S --> (Bottom T) is sups-preserving
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric lower-bounded RelStr holds S --> (Bottom T) is sups-preserving
let T be non empty reflexive antisymmetric lower-bounded RelStr ; ::_thesis: S --> (Bottom T) is sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: S --> (Bottom T) preserves_sup_of X
assume  ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (S --> (Bottom T)) .: X,T & "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) )
set f = the carrier of S --> (Bottom T);
A1: ( the carrier of S --> (Bottom T)) . (sup X) = Bottom T by FUNCOP_1:7;
 (S --> (Bottom T)) .: X c= {(Bottom T)} by FUNCOP_1:81;
then  ( (S --> (Bottom T)) .: X = {(Bottom T)} or (S --> (Bottom T)) .: X = {} ) by ZFMISC_1:33;
hence  ( ex_sup_of (S --> (Bottom T)) .: X,T & "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) ) by A1, YELLOW_0:38, YELLOW_0:39, YELLOW_0:42; ::_thesis: verum
end;

theorem Th42: :: WAYBEL34:42
for S being non empty RelStr
for T being non empty reflexive antisymmetric upper-bounded RelStr holds S --> (Top T) is infs-preserving
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric upper-bounded RelStr holds S --> (Top T) is infs-preserving
let T be non empty reflexive antisymmetric upper-bounded RelStr ; ::_thesis: S --> (Top T) is infs-preserving
let X be Subset of S; :: according to WAYBEL_0:def_32 ::_thesis: S --> (Top T) preserves_inf_of X
assume  ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (S --> (Top T)) .: X,T & "/\" (((S --> (Top T)) .: X),T) = (S --> (Top T)) . ("/\" (X,S)) )
set t = Top T;
set f = the carrier of S --> (Top T);
A1: ( the carrier of S --> (Top T)) . (inf X) = Top T by FUNCOP_1:7;
 (S --> (Top T)) .: X c= {(Top T)} by FUNCOP_1:81;
then  ( (S --> (Top T)) .: X = {(Top T)} or (S --> (Top T)) .: X = {} ) by ZFMISC_1:33;
hence  ( ex_inf_of (S --> (Top T)) .: X,T & "/\" (((S --> (Top T)) .: X),T) = (S --> (Top T)) . ("/\" (X,S)) ) by A1, YELLOW_0:38, YELLOW_0:39, YELLOW_0:43; ::_thesis: verum
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;
clusterS --> (Top T) ->  infs-preserving directed-sups-preserving ;
coherence
 ( S --> (Top T) is directed-sups-preserving & S --> (Top T) is infs-preserving )
proof
thus  S --> (Top T) is directed-sups-preserving ::_thesis: S --> (Top T) is infs-preserving
proof
let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or S --> (Top T) preserves_sup_of X )
thus  ( X is empty or not X is directed or S --> (Top T) preserves_sup_of X ) by Th40; ::_thesis: verum
end;
thus  S --> (Top T) is infs-preserving by Th42; ::_thesis: verum
end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
clusterS --> (Bottom T) ->  sups-preserving filtered-infs-preserving ;
coherence
 ( S --> (Bottom T) is filtered-infs-preserving & S --> (Bottom T) is sups-preserving )
proof
thus  S --> (Bottom T) is filtered-infs-preserving ::_thesis: S --> (Bottom T) is sups-preserving
proof
let X be Subset of S; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or S --> (Bottom T) preserves_inf_of X )
thus  ( X is empty or not X is filtered or S --> (Bottom T) preserves_inf_of X ) by Th40; ::_thesis: verum
end;
thus  S --> (Bottom T) is sups-preserving by Th41; ::_thesis: verum
end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving directed-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st
( b1 is directed-sups-preserving & b1 is infs-preserving )
proof
take  S --> (Top T) ; ::_thesis: ( S --> (Top T) is directed-sups-preserving & S --> (Top T) is infs-preserving )
thus  ( S --> (Top T) is directed-sups-preserving & S --> (Top T) is infs-preserving ) ; ::_thesis: verum
end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving filtered-infs-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st
( b1 is filtered-infs-preserving & b1 is sups-preserving )
proof
take  S --> (Bottom T) ; ::_thesis: ( S --> (Bottom T) is filtered-infs-preserving & S --> (Bottom T) is sups-preserving )
thus  ( S --> (Bottom T) is filtered-infs-preserving & S --> (Bottom T) is sups-preserving ) ; ::_thesis: verum
end;
end;

theorem Th43: :: WAYBEL34:43
for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -INF(SC)_category) iff ( L is strict & L is complete & the carrier of L in W ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE holds
( L is object of (W -INF(SC)_category) iff ( L is strict & L is complete & the carrier of L in W ) )
let L be LATTICE; ::_thesis: ( L is object of (W -INF(SC)_category) iff ( L is strict & L is complete & the carrier of L in W ) )
 the carrier of (W -INF(SC)_category) c= the carrier of (W -INF_category) by ALTCAT_2:def_11;
then  ( L in the carrier of (W -INF(SC)_category) implies L is object of (W -INF_category) ) ;
then  ( L is object of (W -INF(SC)_category) iff L is object of (W -INF_category) ) by Def10;
hence  ( L is object of (W -INF(SC)_category) iff ( L is strict & L is complete & the carrier of L in W ) ) by Th13; ::_thesis: verum
end;

theorem Th44: :: WAYBEL34:44
for W being with_non-empty_element set
for a, b being object of (W -INF(SC)_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -INF(SC)_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
let a, b be object of (W -INF(SC)_category); ::_thesis: for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
let f be set ; ::_thesis: ( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
A1: a in the carrier of (W -INF(SC)_category) ;
A2: b in the carrier of (W -INF(SC)_category) ;
 the carrier of (W -INF(SC)_category) c= the carrier of (W -INF_category) by ALTCAT_2:def_11;
then reconsider a1 = a, b1 = b as object of (W -INF_category) by A1, A2;
hereby  ::_thesis: ( f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> )
assume A3: f in <^a,b^> ; ::_thesis: f is infs-preserving directed-sups-preserving Function of (latt a),(latt b)
A4: <^a,b^> c= <^a1,b1^> by ALTCAT_2:31;
then reconsider g = f as Morphism of a1,b1 by A3;
 f = @ g by A3, A4, YELLOW21:def_7;
hence  f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) by A3, A4, Def10, Th14; ::_thesis: verum
end;
assume  f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) ; ::_thesis: f in <^a,b^>
then reconsider f = f as infs-preserving directed-sups-preserving Function of (latt a),(latt b) ;
A5: f in <^a1,b1^> by Th14;
reconsider g = f as Morphism of a1,b1 by Th14;
 f = @ g by A5, YELLOW21:def_7;
hence  f in <^a,b^> by A5, Def10; ::_thesis: verum
end;

theorem :: WAYBEL34:45
for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -SUP(SO)_category) iff ( L is strict & L is complete & the carrier of L in W ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE holds
( L is object of (W -SUP(SO)_category) iff ( L is strict & L is complete & the carrier of L in W ) )
let L be LATTICE; ::_thesis: ( L is object of (W -SUP(SO)_category) iff ( L is strict & L is complete & the carrier of L in W ) )
 the carrier of (W -SUP(SO)_category) c= the carrier of (W -SUP_category) by ALTCAT_2:def_11;
then  ( L in the carrier of (W -SUP(SO)_category) implies L is object of (W -SUP_category) ) ;
then  ( L is object of (W -SUP(SO)_category) iff L is object of (W -SUP_category) ) by Def11;
hence  ( L is object of (W -SUP(SO)_category) iff ( L is strict & L is complete & the carrier of L in W ) ) by Th15; ::_thesis: verum
end;

theorem Th46: :: WAYBEL34:46
for W being with_non-empty_element set
for a, b being object of (W -SUP(SO)_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -SUP(SO)_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
let a, b be object of (W -SUP(SO)_category); ::_thesis: for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
let f be set ; ::_thesis: ( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
A1: a in the carrier of (W -SUP(SO)_category) ;
A2: b in the carrier of (W -SUP(SO)_category) ;
 the carrier of (W -SUP(SO)_category) c= the carrier of (W -SUP_category) by ALTCAT_2:def_11;
then reconsider a1 = a, b1 = b as object of (W -SUP_category) by A1, A2;
hereby  ::_thesis: ( ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) implies f in <^a,b^> )
assume A3: f in <^a,b^> ; ::_thesis: ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving )
A4: <^a,b^> c= <^a1,b1^> by ALTCAT_2:31;
then reconsider g = f as Morphism of a1,b1 by A3;
A5: f = @ g by A3, A4, YELLOW21:def_7;
A6: UpperAdj (@ g) is directed-sups-preserving by A3, A4, Def11;
 f is sups-preserving Function of (latt a1),(latt b1) by A3, A4, Th16;
hence  ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) by A5, A6; ::_thesis: verum
end;
given g being sups-preserving Function of (latt a),(latt b) such that A7: g = f and
A8: UpperAdj g is directed-sups-preserving ; ::_thesis: f in <^a,b^>
A9: f in <^a1,b1^> by A7, Th16;
reconsider g = f as Morphism of a1,b1 by A7, Th16;
 f = @ g by A9, YELLOW21:def_7;
hence  f in <^a,b^> by A7, A8, A9, Def11; ::_thesis: verum
end;

theorem :: WAYBEL34:47
for W being with_non-empty_element set holds W -INF(SC)_category = Intersect ((W -INF_category),(W -UPS_category))
proof
let W be with_non-empty_element set ; ::_thesis: W -INF(SC)_category = Intersect ((W -INF_category),(W -UPS_category))
consider w being non empty set  such that
A1: w in W by SETFAM_1:def_10;
set r = the well-ordering upper-bounded Order of w;
A2: now__::_thesis:_for_a_being_object_of_(W_-INF_category)
for_b_being_object_of_(W_-UPS_category)_st_a_=_b_holds_
idm_a_=_idm_b
let a be object of (W -INF_category); ::_thesis: for b being object of (W -UPS_category) st a = b holds
idm a = idm b
let b be object of (W -UPS_category); ::_thesis: ( a = b implies idm a = idm b )
 idm a = id (latt a) by YELLOW21:2;
hence  ( a = b implies idm a = idm b ) by YELLOW21:2; ::_thesis: verum
end;
set B = Intersect ((W -INF_category),(W -UPS_category));
A3: W -INF_category ,W -UPS_category have_the_same_composition by YELLOW20:12;
then A4: the carrier of (Intersect ((W -INF_category),(W -UPS_category))) = the carrier of (W -INF_category) /\ the carrier of (W -UPS_category) by YELLOW20:def_3;
A5: RelStr(# w, the well-ordering upper-bounded Order of w #) is object of (W -INF_category) by A1, Th13;
 RelStr(# w, the well-ordering upper-bounded Order of w #) is object of (W -UPS_category) by A1, YELLOW21:14;
then  not Intersect ((W -INF_category),(W -UPS_category)) is empty by A4, A5, XBOOLE_0:def_4;
then reconsider I = Intersect ((W -INF_category),(W -UPS_category)) as non empty subcategory of W -INF_category by A2, YELLOW20:12, YELLOW20:25;
set A = W -INF(SC)_category ;
deffunc H1( set , set ) ->  set = the Arrows of (W -INF(SC)_category) . ($1,$2);
A6: for C1, C2 being semi-functional para-functional category st the carrier of C1 = the carrier of (W -INF(SC)_category) & ( for a, b being object of C1 holds <^a,b^> = H1(a,b) ) & the carrier of C2 = the carrier of (W -INF(SC)_category) & ( for a, b being object of C2 holds <^a,b^> = H1(a,b) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW18:sch_19();
A7: the carrier of I = the carrier of (W -INF(SC)_category)
proof
thus  the carrier of I c= the carrier of (W -INF(SC)_category) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (W -INF(SC)_category) c= the carrier of I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of I or x in the carrier of (W -INF(SC)_category) )
assume  x in the carrier of I ; ::_thesis: x in the carrier of (W -INF(SC)_category)
then reconsider x = x as object of I ;
reconsider L = x as LATTICE by YELLOW21:def_4;
A8: x in the carrier of (W -UPS_category) by A4, XBOOLE_0:def_4;
then A9: ( L is strict & L is complete ) by A1, YELLOW21:def_10;
 the carrier of L in W by A1, A8, YELLOW21:def_10;
then  L is object of (W -INF(SC)_category) by A9, Th43;
hence  x in the carrier of (W -INF(SC)_category) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W -INF(SC)_category) or x in the carrier of I )
assume  x in the carrier of (W -INF(SC)_category) ; ::_thesis: x in the carrier of I
then reconsider x = x as object of (W -INF(SC)_category) ;
reconsider L = x as LATTICE by YELLOW21:def_4;
A10: ( L is complete & L is strict ) by Th43;
A11: the carrier of L in W by Th43;
then A12: x is object of (W -INF_category) by A10, Th13;
 x is object of (W -UPS_category) by A10, A11, YELLOW21:def_10;
hence  x in the carrier of I by A4, A12, XBOOLE_0:def_4; ::_thesis: verum
end;
A13: for a, b being object of (W -INF(SC)_category) holds <^a,b^> = H1(a,b) by ALTCAT_1:def_1;
now__::_thesis:_for_a,_b_being_object_of_I_holds_<^a,b^>_=_H1(a,b)
let a, b be object of I; ::_thesis: <^a,b^> = H1(a,b)
reconsider a9 = a, b9 = b as object of (W -INF(SC)_category) by A7;
reconsider a1 = a, b1 = b as object of (W -INF_category) by A4, XBOOLE_0:def_4;
reconsider a2 = a, b2 = b as object of (W -UPS_category) by A4, XBOOLE_0:def_4;
A14: dom the Arrows of (W -INF_category) = [: the carrier of (W -INF_category), the carrier of (W -INF_category):] by PARTFUN1:def_2;
 dom the Arrows of (W -UPS_category) = [: the carrier of (W -UPS_category), the carrier of (W -UPS_category):] by PARTFUN1:def_2;
then A15: (dom the Arrows of (W -INF_category)) /\ (dom the Arrows of (W -UPS_category)) = [:( the carrier of (W -INF_category) /\ the carrier of (W -UPS_category)),( the carrier of (W -INF_category) /\ the carrier of (W -UPS_category)):] by A14, ZFMISC_1:100;
A16: <^a,b^> = the Arrows of I . (a,b) by ALTCAT_1:def_1
.= (Intersect ( the Arrows of (W -INF_category), the Arrows of (W -UPS_category))) . [a,b] by A3, YELLOW20:def_3
.= ( the Arrows of (W -INF_category) . (a,b)) /\ ( the Arrows of (W -UPS_category) . [a,b]) by A4, A15, YELLOW20:def_2
.= <^a1,b1^> /\ ( the Arrows of (W -UPS_category) . (a,b)) by ALTCAT_1:def_1
.= <^a1,b1^> /\ <^a2,b2^> by ALTCAT_1:def_1 ;
now__::_thesis:_for_f_being_set_holds_
(_f_in_<^a,b^>_iff_f_in_H1(a,b)_)
let f be set ; ::_thesis: ( f in <^a,b^> iff f in H1(a,b) )
 ( f in <^a,b^> iff ( f in <^a1,b1^> & f in <^a2,b2^> ) ) by A16, XBOOLE_0:def_4;
then  ( f in <^a,b^> iff ( f is directed-sups-preserving Function of (latt a2),(latt b2) & f is infs-preserving Function of (latt a1),(latt b1) ) ) by Th14, YELLOW21:15;
then  ( f in <^a,b^> iff f in <^a9,b9^> ) by Th44;
hence  ( f in <^a,b^> iff f in H1(a,b) ) by ALTCAT_1:def_1; ::_thesis: verum
end;
hence  <^a,b^> = H1(a,b) by TARSKI:1; ::_thesis: verum
end;
hence  W -INF(SC)_category = Intersect ((W -INF_category),(W -UPS_category)) by A6, A7, A13; ::_thesis: verum
end;

definition
let W be with_non-empty_element set ;
defpred S1[ object of (W -INF(SC)_category)] means  latt $1 is continuous ;
consider a being non empty set  such that
A1: a in W by SETFAM_1:def_10;
set r = the well-ordering upper-bounded Order of a;
set b = RelStr(# a, the well-ordering upper-bounded Order of a #);
funcW -CL_category  ->  non empty strict full subcategory of W -INF(SC)_category  means :Def12: :: WAYBEL34:def 12
 for a being object of (W -INF(SC)_category) holds
( a is object of it iff latt a is continuous );
existence
 ex b1 being non empty strict full subcategory of W -INF(SC)_category st
for a being object of (W -INF(SC)_category) holds
( a is object of b1 iff latt a is continuous )
proof
 RelStr(# a, the well-ordering upper-bounded Order of a #) is object of (W -INF_category) by A1, Def4;
then reconsider b = RelStr(# a, the well-ordering upper-bounded Order of a #) as object of (W -INF(SC)_category) by Def10;
 b = latt b ;
then A2: ex b being object of (W -INF(SC)_category) st S1[b] ;
thus  ex B being non empty strict full subcategory of W -INF(SC)_category st
for a being object of (W -INF(SC)_category) holds
( a is object of B iff S1[a] ) from YELLOW20:sch_2(A2); ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -INF(SC)_category st ( for a being object of (W -INF(SC)_category) holds
( a is object of b1 iff latt a is continuous ) ) & ( for a being object of (W -INF(SC)_category) holds
( a is object of b2 iff latt a is continuous ) ) holds
b1 = b2;
proof
let B1, B2 be non empty strict full subcategory of W -INF(SC)_category ; ::_thesis: ( ( for a being object of (W -INF(SC)_category) holds
( a is object of B1 iff latt a is continuous ) ) & ( for a being object of (W -INF(SC)_category) holds
( a is object of B2 iff latt a is continuous ) ) implies B1 = B2 )
assume that
A3: for a being object of (W -INF(SC)_category) holds
( a is object of B1 iff S1[a] ) and
A4: for a being object of (W -INF(SC)_category) holds
( a is object of B2 iff S1[a] ) ; ::_thesis: B1 = B2
 AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch_3(A3, A4);
hence  B1 = B2 ; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines -CL_category WAYBEL34:def_12_:_
 for W being with_non-empty_element set
for b2 being non empty strict full subcategory of W -INF(SC)_category holds
( b2 = W -CL_category iff for a being object of (W -INF(SC)_category) holds
( a is object of b2 iff latt a is continuous ) );

registration
let W be with_non-empty_element set ;
clusterW -CL_category  ->  non empty strict full with_complete_lattices ;
coherence
 W -CL_category is with_complete_lattices ;
end;

theorem Th48: :: WAYBEL34:48
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is object of (W -CL_category) iff ( L is strict & L is complete & L is continuous ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE st the carrier of L in W holds
( L is object of (W -CL_category) iff ( L is strict & L is complete & L is continuous ) )
A1: ex a being non empty set st a in W by SETFAM_1:def_10;
A2: the carrier of (W -INF(SC)_category) c= the carrier of (W -INF_category) by ALTCAT_2:def_11;
A3: the carrier of (W -CL_category) c= the carrier of (W -INF(SC)_category) by ALTCAT_2:def_11;
let L be LATTICE; ::_thesis: ( the carrier of L in W implies ( L is object of (W -CL_category) iff ( L is strict & L is complete & L is continuous ) ) )
assume A4: the carrier of L in W ; ::_thesis: ( L is object of (W -CL_category) iff ( L is strict & L is complete & L is continuous ) )
hereby  ::_thesis: ( L is strict & L is complete & L is continuous implies L is object of (W -CL_category) )
assume A5: L is object of (W -CL_category) ; ::_thesis: ( L is strict & L is complete & L is continuous )
then  L in the carrier of (W -CL_category) ;
then reconsider a = L as object of (W -INF(SC)_category) by A3;
A6: a in the carrier of (W -INF(SC)_category) ;
 latt a is continuous by A5, Def12;
hence  ( L is strict & L is complete & L is continuous ) by A1, A2, A6, Def4; ::_thesis: verum
end;
assume A7: ( L is strict & L is complete & L is continuous ) ; ::_thesis: L is object of (W -CL_category)
then  L is object of (W -INF_category) by A4, Def4;
then reconsider a = L as object of (W -INF(SC)_category) by Def10;
 latt a = L ;
hence  L is object of (W -CL_category) by A7, Def12; ::_thesis: verum
end;

theorem Th49: :: WAYBEL34:49
for W being with_non-empty_element set
for a, b being object of (W -CL_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -CL_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
let a, b be object of (W -CL_category); ::_thesis: for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
let f be set ; ::_thesis: ( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
A1: a in the carrier of (W -CL_category) ;
A2: b in the carrier of (W -CL_category) ;
 the carrier of (W -CL_category) c= the carrier of (W -INF(SC)_category) by ALTCAT_2:def_11;
then reconsider a1 = a, b1 = b as object of (W -INF(SC)_category) by A1, A2;
 <^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence  ( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) ) by Th44; ::_thesis: verum
end;

definition
let W be with_non-empty_element set ;
defpred S1[ object of (W -SUP(SO)_category)] means  latt $1 is continuous ;
consider a being non empty set  such that
A1: a in W by SETFAM_1:def_10;
set r = the well-ordering upper-bounded Order of a;
set b = RelStr(# a, the well-ordering upper-bounded Order of a #);
funcW -CL-opp_category  ->  non empty strict full subcategory of W -SUP(SO)_category  means :Def13: :: WAYBEL34:def 13
 for a being object of (W -SUP(SO)_category) holds
( a is object of it iff latt a is continuous );
existence
 ex b1 being non empty strict full subcategory of W -SUP(SO)_category st
for a being object of (W -SUP(SO)_category) holds
( a is object of b1 iff latt a is continuous )
proof
 RelStr(# a, the well-ordering upper-bounded Order of a #) is object of (W -SUP_category) by A1, Def5;
then reconsider b = RelStr(# a, the well-ordering upper-bounded Order of a #) as object of (W -SUP(SO)_category) by Def11;
 b = latt b ;
then A2: ex b being object of (W -SUP(SO)_category) st S1[b] ;
thus  ex B being non empty strict full subcategory of W -SUP(SO)_category st
for a being object of (W -SUP(SO)_category) holds
( a is object of B iff S1[a] ) from YELLOW20:sch_2(A2); ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -SUP(SO)_category st ( for a being object of (W -SUP(SO)_category) holds
( a is object of b1 iff latt a is continuous ) ) & ( for a being object of (W -SUP(SO)_category) holds
( a is object of b2 iff latt a is continuous ) ) holds
b1 = b2;
proof
let B1, B2 be non empty strict full subcategory of W -SUP(SO)_category ; ::_thesis: ( ( for a being object of (W -SUP(SO)_category) holds
( a is object of B1 iff latt a is continuous ) ) & ( for a being object of (W -SUP(SO)_category) holds
( a is object of B2 iff latt a is continuous ) ) implies B1 = B2 )
assume that
A3: for a being object of (W -SUP(SO)_category) holds
( a is object of B1 iff S1[a] ) and
A4: for a being object of (W -SUP(SO)_category) holds
( a is object of B2 iff S1[a] ) ; ::_thesis: B1 = B2
 AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch_3(A3, A4);
hence  B1 = B2 ; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines -CL-opp_category WAYBEL34:def_13_:_
 for W being with_non-empty_element set
for b2 being non empty strict full subcategory of W -SUP(SO)_category holds
( b2 = W -CL-opp_category iff for a being object of (W -SUP(SO)_category) holds
( a is object of b2 iff latt a is continuous ) );

theorem Th50: :: WAYBEL34:50
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is object of (W -CL-opp_category) iff ( L is strict & L is complete & L is continuous ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE st the carrier of L in W holds
( L is object of (W -CL-opp_category) iff ( L is strict & L is complete & L is continuous ) )
A1: ex a being non empty set st a in W by SETFAM_1:def_10;
A2: the carrier of (W -SUP(SO)_category) c= the carrier of (W -SUP_category) by ALTCAT_2:def_11;
A3: the carrier of (W -CL-opp_category) c= the carrier of (W -SUP(SO)_category) by ALTCAT_2:def_11;
let L be LATTICE; ::_thesis: ( the carrier of L in W implies ( L is object of (W -CL-opp_category) iff ( L is strict & L is complete & L is continuous ) ) )
assume A4: the carrier of L in W ; ::_thesis: ( L is object of (W -CL-opp_category) iff ( L is strict & L is complete & L is continuous ) )
hereby  ::_thesis: ( L is strict & L is complete & L is continuous implies L is object of (W -CL-opp_category) )
assume A5: L is object of (W -CL-opp_category) ; ::_thesis: ( L is strict & L is complete & L is continuous )
then  L in the carrier of (W -CL-opp_category) ;
then reconsider a = L as object of (W -SUP(SO)_category) by A3;
A6: a in the carrier of (W -SUP(SO)_category) ;
 latt a is continuous by A5, Def13;
hence  ( L is strict & L is complete & L is continuous ) by A1, A2, A6, Def5; ::_thesis: verum
end;
assume A7: ( L is strict & L is complete & L is continuous ) ; ::_thesis: L is object of (W -CL-opp_category)
then  L is object of (W -SUP_category) by A4, Def5;
then reconsider a = L as object of (W -SUP(SO)_category) by Def11;
 latt a = L ;
hence  L is object of (W -CL-opp_category) by A7, Def13; ::_thesis: verum
end;

theorem Th51: :: WAYBEL34:51
for W being with_non-empty_element set
for a, b being object of (W -CL-opp_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -CL-opp_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
let a, b be object of (W -CL-opp_category); ::_thesis: for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
let f be set ; ::_thesis: ( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
A1: a in the carrier of (W -CL-opp_category) ;
A2: b in the carrier of (W -CL-opp_category) ;
 the carrier of (W -CL-opp_category) c= the carrier of (W -SUP(SO)_category) by ALTCAT_2:def_11;
then reconsider a1 = a, b1 = b as object of (W -SUP(SO)_category) by A1, A2;
 <^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence  ( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) ) by Th46; ::_thesis: verum
end;

theorem Th52: :: WAYBEL34:52
for W being with_non-empty_element set holds W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj
proof
let W be with_non-empty_element set ; ::_thesis: W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj
set A1 = W -INF_category ;
set B1 = W -INF(SC)_category ;
set B2 = W -SUP(SO)_category ;
set F = W LowerAdj ;
A1: ex a being non empty set st a in W by SETFAM_1:def_10;
A2: for a being object of (W -INF_category) holds
( a is object of (W -INF(SC)_category) iff (W LowerAdj) . a is object of (W -SUP(SO)_category) ) by Def10, Def11;
A3: now__::_thesis:_for_a,_b_being_object_of_(W_-INF_category)_st_<^a,b^>_<>_{}_holds_
for_a1,_b1_being_object_of_(W_-INF(SC)_category)_st_a1_=_a_&_b1_=_b_holds_
for_a2,_b2_being_object_of_(W_-SUP(SO)_category)_st_a2_=_(W_LowerAdj)_._a_&_b2_=_(W_LowerAdj)_._b_holds_
for_f_being_Morphism_of_a,b_holds_
(_f_in_<^a1,b1^>_iff_(W_LowerAdj)_._f_in_<^b2,a2^>_)
let a, b be object of (W -INF_category); ::_thesis: ( <^a,b^> <> {} implies for a1, b1 being object of (W -INF(SC)_category) st a1 = a & b1 = b holds
for a2, b2 being object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> ) )
assume A4: <^a,b^> <> {} ; ::_thesis: for a1, b1 being object of (W -INF(SC)_category) st a1 = a & b1 = b holds
for a2, b2 being object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )
let a1, b1 be object of (W -INF(SC)_category); ::_thesis: ( a1 = a & b1 = b implies for a2, b2 being object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> ) )
assume that
A5: a1 = a and
A6: b1 = b ; ::_thesis: for a2, b2 being object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )
let a2, b2 be object of (W -SUP(SO)_category); ::_thesis: ( a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b implies for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> ) )
assume that
A7: a2 = (W LowerAdj) . a and
A8: b2 = (W LowerAdj) . b ; ::_thesis: for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )
let f be Morphism of a,b; ::_thesis: ( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )
A9: <^((W LowerAdj) . b),((W LowerAdj) . a)^> <> {} by A4, FUNCTOR0:def_19;
A10: @ f = f by A4, YELLOW21:def_7;
A11: @ ((W LowerAdj) . f) = (W LowerAdj) . f by A9, YELLOW21:def_7;
A12: (W LowerAdj) . a = latt a by Def6;
A13: (W LowerAdj) . b = latt b by Def6;
A14: (W LowerAdj) . f = LowerAdj (@ f) by A4, Def6;
reconsider g = f as infs-preserving Function of (latt a1),(latt b1) by A1, A4, A5, A6, A10, Def4;
 UpperAdj (LowerAdj g) = g by Th10;
then  ( f in <^a1,b1^> iff UpperAdj (LowerAdj g) is directed-sups-preserving ) by A4, A5, A6, A10, Def10;
hence  ( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> ) by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Def11; ::_thesis: verum
end;
thus  W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj by A2, A3, YELLOW20:57; ::_thesis: verum
end;

theorem :: WAYBEL34:53
for W being with_non-empty_element set holds W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under W UpperAdj
proof
let W be with_non-empty_element set ; ::_thesis: W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under W UpperAdj
 W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under (W LowerAdj) " by Th52, YELLOW20:51;
hence  W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under W UpperAdj by Th18; ::_thesis: verum
end;

theorem Th54: :: WAYBEL34:54
for W being with_non-empty_element set holds W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj
proof
let W be with_non-empty_element set ; ::_thesis: W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj
set A1 = W -INF_category ;
set A2 = W -SUP_category ;
reconsider B1 = W -CL_category as non empty subcategory of W -INF_category by ALTCAT_4:36;
reconsider B2 = W -CL-opp_category as non empty subcategory of W -SUP_category by ALTCAT_4:36;
set F = W LowerAdj ;
A1: ex a being non empty set st a in W by SETFAM_1:def_10;
A2: for a being object of (W -INF_category) holds
( a is object of B1 iff (W LowerAdj) . a is object of B2 )
proof
let a be object of (W -INF_category); ::_thesis: ( a is object of B1 iff (W LowerAdj) . a is object of B2 )
A3: (W LowerAdj) . a = latt a by Def6;
A4: the carrier of (latt a) in W by A1, Def4;
then  ( a is object of B1 iff ( latt a is strict & latt a is complete & latt a is continuous ) ) by Th48;
hence  ( a is object of B1 iff (W LowerAdj) . a is object of B2 ) by A3, A4, Th50; ::_thesis: verum
end;
A5: now__::_thesis:_for_a,_b_being_object_of_(W_-INF_category)_st_<^a,b^>_<>_{}_holds_
for_a1,_b1_being_object_of_B1_st_a1_=_a_&_b1_=_b_holds_
for_a2,_b2_being_object_of_B2_st_a2_=_(W_LowerAdj)_._a_&_b2_=_(W_LowerAdj)_._b_holds_
for_f_being_Morphism_of_a,b_holds_
(_(_f_in_<^a1,b1^>_implies_(W_LowerAdj)_._f_in_<^b2,a2^>_)_&_(_(W_LowerAdj)_._f_in_<^b2,a2^>_implies_f_in_<^a1,b1^>_)_)
let a, b be object of (W -INF_category); ::_thesis: ( <^a,b^> <> {} implies for a1, b1 being object of B1 st a1 = a & b1 = b holds
for a2, b2 being object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )
assume A6: <^a,b^> <> {} ; ::_thesis: for a1, b1 being object of B1 st a1 = a & b1 = b holds
for a2, b2 being object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )
let a1, b1 be object of B1; ::_thesis: ( a1 = a & b1 = b implies for a2, b2 being object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )
assume that
A7: a1 = a and
A8: b1 = b ; ::_thesis: for a2, b2 being object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )
let a2, b2 be object of B2; ::_thesis: ( a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b implies for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )
assume that
A9: a2 = (W LowerAdj) . a and
A10: b2 = (W LowerAdj) . b ; ::_thesis: for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )
let f be Morphism of a,b; ::_thesis: ( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )
A11: @ f = f by A6, YELLOW21:def_7;
A12: (W LowerAdj) . a = latt a by Def6;
A13: (W LowerAdj) . b = latt b by Def6;
A14: (W LowerAdj) . f = LowerAdj (@ f) by A6, Def6;
reconsider g = f as infs-preserving Function of (latt a1),(latt b1) by A1, A6, A7, A8, A11, Def4;
A15: UpperAdj (LowerAdj g) = g by Th10;
then  ( f in <^a1,b1^> iff UpperAdj (LowerAdj g) is directed-sups-preserving ) by Th49;
hence  ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) by A7, A8, A9, A10, A11, A12, A13, A14, Th51; ::_thesis: ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> )
assume  (W LowerAdj) . f in <^b2,a2^> ; ::_thesis: f in <^a1,b1^>
then  ex g being sups-preserving Function of (latt b2),(latt a2) st
( (W LowerAdj) . f = g & UpperAdj g is directed-sups-preserving ) by Th51;
hence  f in <^a1,b1^> by A7, A8, A9, A10, A11, A12, A13, A14, A15, Th49; ::_thesis: verum
end;
 B1,B2 are_anti-isomorphic_under W LowerAdj by A2, A5, YELLOW20:57;
hence  W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj ; ::_thesis: verum
end;

theorem :: WAYBEL34:55
for W being with_non-empty_element set holds W -CL-opp_category ,W -CL_category are_anti-isomorphic_under W UpperAdj
proof
let W be with_non-empty_element set ; ::_thesis: W -CL-opp_category ,W -CL_category are_anti-isomorphic_under W UpperAdj
set A1 = W -INF_category ;
set A2 = W -SUP_category ;
reconsider B1 = W -CL_category as non empty subcategory of W -INF_category by ALTCAT_4:36;
reconsider B2 = W -CL-opp_category as non empty subcategory of W -SUP_category by ALTCAT_4:36;
 B2,B1 are_anti-isomorphic_under (W LowerAdj) " by Th54, YELLOW20:51;
hence  W -CL-opp_category ,W -CL_category are_anti-isomorphic_under W UpperAdj by Th18; ::_thesis: verum
end;

begin

definition
let S, T be non empty reflexive RelStr ;
let f be Function of S,T;
attrf is compact-preserving  means :: WAYBEL34:def 14
 for s being Element of S st s is compact holds
f . s is compact ;
end;

:: deftheorem  defines compact-preserving WAYBEL34:def_14_:_
 for S, T being non empty reflexive RelStr
for f being Function of S,T holds
( f is compact-preserving iff for s being Element of S st s is compact holds
f . s is compact );

theorem Th56: :: WAYBEL34:56
for S, T being complete LATTICE
for d being sups-preserving Function of T,S st d is waybelow-preserving holds
d is compact-preserving
proof
let S, T be complete LATTICE; ::_thesis: for d being sups-preserving Function of T,S st d is waybelow-preserving holds
d is compact-preserving
let d be sups-preserving Function of T,S; ::_thesis: ( d is waybelow-preserving implies d is compact-preserving )
assume A1: for t, t9 being Element of T st t << t9 holds
d . t << d . t9 ; :: according to WAYBEL34:def_8 ::_thesis: d is compact-preserving
let t be Element of T; :: according to WAYBEL34:def_14 ::_thesis: ( t is compact implies d . t is compact )
assume  t << t ; :: according to WAYBEL_3:def_2 ::_thesis: d . t is compact
hence  d . t << d . t by A1; :: according to WAYBEL_3:def_2 ::_thesis: verum
end;

theorem Th57: :: WAYBEL34:57
for S, T being complete LATTICE
for d being sups-preserving Function of T,S st T is algebraic & d is compact-preserving holds
d is waybelow-preserving
proof
let S, T be complete LATTICE; ::_thesis: for d being sups-preserving Function of T,S st T is algebraic & d is compact-preserving holds
d is waybelow-preserving
let d be sups-preserving Function of T,S; ::_thesis: ( T is algebraic & d is compact-preserving implies d is waybelow-preserving )
assume that
A1: T is algebraic and
A2: for t being Element of T st t is compact holds
d . t is compact ; :: according to WAYBEL34:def_14 ::_thesis: d is waybelow-preserving
let t, t9 be Element of T; :: according to WAYBEL34:def_8 ::_thesis: ( t << t9 implies d . t << d . t9 )
assume  t << t9 ; ::_thesis: d . t << d . t9
then consider k being Element of T such that
A3: k in the carrier of (CompactSublatt T) and
A4: t <= k and
A5: k <= t9 by A1, WAYBEL_8:7;
 k is compact by A3, WAYBEL_8:def_1;
then  d . k is compact by A2;
then A6: d . k << d . k by WAYBEL_3:def_2;
A7: d . t <= d . k by A4, WAYBEL_1:def_2;
 d . k <= d . t9 by A5, WAYBEL_1:def_2;
hence  d . t << d . t9 by A6, A7, WAYBEL_3:2; ::_thesis: verum
end;

theorem Th58: :: WAYBEL34:58
for R, S, T being non empty RelStr
for X being Subset of R
for f being Function of R,S
for g being Function of S,T st f preserves_sup_of X & g preserves_sup_of f .: X holds
g * f preserves_sup_of X
proof
let R, S, T be non empty RelStr ; ::_thesis: for X being Subset of R
for f being Function of R,S
for g being Function of S,T st f preserves_sup_of X & g preserves_sup_of f .: X holds
g * f preserves_sup_of X
let X be Subset of R; ::_thesis: for f being Function of R,S
for g being Function of S,T st f preserves_sup_of X & g preserves_sup_of f .: X holds
g * f preserves_sup_of X
let f be Function of R,S; ::_thesis: for g being Function of S,T st f preserves_sup_of X & g preserves_sup_of f .: X holds
g * f preserves_sup_of X
let g be Function of S,T; ::_thesis: ( f preserves_sup_of X & g preserves_sup_of f .: X implies g * f preserves_sup_of X )
assume that
A1: ( ex_sup_of X,R implies ( ex_sup_of f .: X,S & sup (f .: X) = f . (sup X) ) ) and
A2: ( ex_sup_of f .: X,S implies ( ex_sup_of g .: (f .: X),T & sup (g .: (f .: X)) = g . (sup (f .: X)) ) ) ; :: according to WAYBEL_0:def_31 ::_thesis: g * f preserves_sup_of X
A3: g .: (f .: X) = (g * f) .: X by RELAT_1:126;
assume  ex_sup_of X,R ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (g * f) .: X,T & "\/" (((g * f) .: X),T) = (g * f) . ("\/" (X,R)) )
hence  ( ex_sup_of (g * f) .: X,T & "\/" (((g * f) .: X),T) = (g * f) . ("\/" (X,R)) ) by A1, A2, A3, FUNCT_2:15; ::_thesis: verum
end;

definition
let S, T be non empty RelStr ;
let f be Function of S,T;
attrf is finite-sups-preserving  means :: WAYBEL34:def 15
 for X being finite Subset of S holds f preserves_sup_of X;
attrf is bottom-preserving  means :Def16: :: WAYBEL34:def 16
f preserves_sup_of {} S;
end;

:: deftheorem  defines finite-sups-preserving WAYBEL34:def_15_:_
 for S, T being non empty RelStr
for f being Function of S,T holds
( f is finite-sups-preserving iff for X being finite Subset of S holds f preserves_sup_of X );

:: deftheorem Def16 defines bottom-preserving WAYBEL34:def_16_:_
 for S, T being non empty RelStr
for f being Function of S,T holds
( f is bottom-preserving iff f preserves_sup_of {} S );

theorem :: WAYBEL34:59
for R, S, T being non empty RelStr
for f being Function of R,S
for g being Function of S,T st f is finite-sups-preserving & g is finite-sups-preserving holds
g * f is finite-sups-preserving
proof
let R, S, T be non empty RelStr ; ::_thesis: for f being Function of R,S
for g being Function of S,T st f is finite-sups-preserving & g is finite-sups-preserving holds
g * f is finite-sups-preserving
let f be Function of R,S; ::_thesis: for g being Function of S,T st f is finite-sups-preserving & g is finite-sups-preserving holds
g * f is finite-sups-preserving
let g be Function of S,T; ::_thesis: ( f is finite-sups-preserving & g is finite-sups-preserving implies g * f is finite-sups-preserving )
assume that
A1: for X being finite Subset of R holds f preserves_sup_of X and
A2: for X being finite Subset of S holds g preserves_sup_of X ; :: according to WAYBEL34:def_15 ::_thesis: g * f is finite-sups-preserving
let X be finite Subset of R; :: according to WAYBEL34:def_15 ::_thesis: g * f preserves_sup_of X
 g preserves_sup_of f .: X by A2;
hence  g * f preserves_sup_of X by A1, Th58; ::_thesis: verum
end;

definition
let S, T be non empty antisymmetric lower-bounded RelStr ;
let f be Function of S,T;
redefine attr f is bottom-preserving  means :Def17: :: WAYBEL34:def 17
f . (Bottom S) = Bottom T;
compatibility
 ( f is bottom-preserving iff f . (Bottom S) = Bottom T )
proof
thus  ( f is bottom-preserving implies f . (Bottom S) = Bottom T ) ::_thesis: ( f . (Bottom S) = Bottom T implies f is bottom-preserving )
proof
assume  f preserves_sup_of {} S ; :: according to WAYBEL34:def_16 ::_thesis: f . (Bottom S) = Bottom T
then  ( ex_sup_of {} S,S implies sup (f .: ({} S)) = f . (sup ({} S)) ) by WAYBEL_0:def_31;
hence  f . (Bottom S) = Bottom T by YELLOW_0:42; ::_thesis: verum
end;
assume that
A1: f . (Bottom S) = Bottom T and
 ex_sup_of {} S,S ; :: according to WAYBEL_0:def_31,WAYBEL34:def_16 ::_thesis: ( ex_sup_of f .: ({} S),T & "\/" ((f .: ({} S)),T) = f . ("\/" (({} S),S)) )
thus  ex_sup_of f .: ({} S),T by YELLOW_0:42; ::_thesis: "\/" ((f .: ({} S)),T) = f . ("\/" (({} S),S))
thus  "\/" ((f .: ({} S)),T) = f . ("\/" (({} S),S)) by A1; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines bottom-preserving WAYBEL34:def_17_:_
 for S, T being non empty antisymmetric lower-bounded RelStr
for f being Function of S,T holds
( f is bottom-preserving iff f . (Bottom S) = Bottom T );

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
attrS is finite-sups-inheriting  means :Def18: :: WAYBEL34:def 18
 for X being finite Subset of S st ex_sup_of X,L holds
"\/" (X,L) in the carrier of S;
attrS is bottom-inheriting  means :Def19: :: WAYBEL34:def 19
 Bottom L in the carrier of S;
end;

:: deftheorem Def18 defines finite-sups-inheriting WAYBEL34:def_18_:_
 for L being non empty RelStr
for S being SubRelStr of L holds
( S is finite-sups-inheriting iff for X being finite Subset of S st ex_sup_of X,L holds
"\/" (X,L) in the carrier of S );

:: deftheorem Def19 defines bottom-inheriting WAYBEL34:def_19_:_
 for L being non empty RelStr
for S being SubRelStr of L holds
( S is bottom-inheriting iff Bottom L in the carrier of S );

registration
let S, T be non empty RelStr ;
cluster Function-like quasi_total sups-preserving  ->  bottom-preserving for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is sups-preserving holds
b1 is bottom-preserving
proof
let f be Function of S,T; ::_thesis: ( f is sups-preserving implies f is bottom-preserving )
assume  f is sups-preserving ; ::_thesis: f is bottom-preserving
hence  f preserves_sup_of {} S by WAYBEL_0:def_33; :: according to WAYBEL34:def_16 ::_thesis: verum
end;
end;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
cluster finite-sups-inheriting  ->  join-inheriting bottom-inheriting for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is finite-sups-inheriting holds
( b1 is bottom-inheriting & b1 is join-inheriting )
proof
let S be SubRelStr of L; ::_thesis: ( S is finite-sups-inheriting implies ( S is bottom-inheriting & S is join-inheriting ) )
assume A1: S is finite-sups-inheriting ; ::_thesis: ( S is bottom-inheriting & S is join-inheriting )
then  ( ex_sup_of {} ,L implies "\/" (({} S),L) in the carrier of S ) by Def18;
hence  Bottom L in the carrier of S by YELLOW_0:42; :: according to WAYBEL34:def_19 ::_thesis: S is join-inheriting
let x, y be Element of L; :: according to YELLOW_0:def_17 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_sup_of {x,y},L or "\/" ({x,y},L) in the carrier of S )
assume that
A2: x in the carrier of S and
A3: y in the carrier of S ; ::_thesis: ( not ex_sup_of {x,y},L or "\/" ({x,y},L) in the carrier of S )
reconsider X = {x,y} as finite Subset of S by A2, A3, ZFMISC_1:32;
 ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) by A1, Def18;
hence  ( not ex_sup_of {x,y},L or "\/" ({x,y},L) in the carrier of S ) ; ::_thesis: verum
end;
end;

registration
let L be non empty RelStr ;
cluster sups-inheriting  ->  finite-sups-inheriting for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is sups-inheriting holds
b1 is finite-sups-inheriting
proof
let S be SubRelStr of L; ::_thesis: ( S is sups-inheriting implies S is finite-sups-inheriting )
assume A1: S is sups-inheriting ; ::_thesis: S is finite-sups-inheriting
let X be finite Subset of S; :: according to WAYBEL34:def_18 ::_thesis: ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S )
thus  ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) by A1, YELLOW_0:def_19; ::_thesis: verum
end;
end;

registration
let S, T be non empty lower-bounded Poset;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st b1 is sups-preserving
proof
set f = the sups-preserving Function of S,T;
take  the sups-preserving Function of S,T ; ::_thesis: the sups-preserving Function of S,T is sups-preserving
thus  the sups-preserving Function of S,T is sups-preserving ; ::_thesis: verum
end;
end;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
cluster full bottom-inheriting  ->  non empty lower-bounded full for SubRelStr of L;
coherence
 for b1 being full SubRelStr of L st b1 is bottom-inheriting holds
( not b1 is empty & b1 is lower-bounded )
proof
let S be full SubRelStr of L; ::_thesis: ( S is bottom-inheriting implies ( not S is empty & S is lower-bounded ) )
assume A1: Bottom L in the carrier of S ; :: according to WAYBEL34:def_19 ::_thesis: ( not S is empty & S is lower-bounded )
hence A2: not S is empty ; ::_thesis: S is lower-bounded
reconsider x = Bottom L as Element of S by A1;
take  x ; :: according to YELLOW_0:def_4 ::_thesis: x is_<=_than the carrier of S
let y be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not y in the carrier of S or x <= y )
assume A3: y in the carrier of S ; ::_thesis: x <= y
reconsider a = y as Element of L by A2, YELLOW_0:58;
 Bottom L <= a by YELLOW_0:44;
hence  x <= y by A3, YELLOW_0:60; ::_thesis: verum
end;
end;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
cluster non empty full sups-inheriting finite-sups-inheriting bottom-inheriting for SubRelStr of L;
existence
 ex b1 being SubRelStr of L st
( not b1 is empty & b1 is sups-inheriting & b1 is finite-sups-inheriting & b1 is bottom-inheriting & b1 is full )
proof
set S = the non empty full sups-inheriting SubRelStr of L;
take  the non empty full sups-inheriting SubRelStr of L ; ::_thesis: ( not the non empty full sups-inheriting SubRelStr of L is empty & the non empty full sups-inheriting SubRelStr of L is sups-inheriting & the non empty full sups-inheriting SubRelStr of L is finite-sups-inheriting & the non empty full sups-inheriting SubRelStr of L is bottom-inheriting & the non empty full sups-inheriting SubRelStr of L is full )
thus  ( not the non empty full sups-inheriting SubRelStr of L is empty & the non empty full sups-inheriting SubRelStr of L is sups-inheriting & the non empty full sups-inheriting SubRelStr of L is finite-sups-inheriting & the non empty full sups-inheriting SubRelStr of L is bottom-inheriting & the non empty full sups-inheriting SubRelStr of L is full ) ; ::_thesis: verum
end;
end;

theorem Th60: :: WAYBEL34:60
for L being non empty antisymmetric lower-bounded RelStr
for S being non empty full bottom-inheriting SubRelStr of L holds Bottom S = Bottom L
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for S being non empty full bottom-inheriting SubRelStr of L holds Bottom S = Bottom L
let S be non empty full bottom-inheriting SubRelStr of L; ::_thesis: Bottom S = Bottom L
reconsider s = Bottom L as Element of S by Def19;
reconsider l = Bottom S as Element of L by YELLOW_0:58;
A1: Bottom L <= l by YELLOW_0:44;
A2: Bottom S <= s by YELLOW_0:44;
 Bottom S >= s by A1, YELLOW_0:60;
hence  Bottom S = Bottom L by A2, ORDERS_2:2; ::_thesis: verum
end;

registration
let L be non empty lower-bounded with_suprema Poset;
cluster full join-inheriting bottom-inheriting  ->  full finite-sups-inheriting for SubRelStr of L;
coherence
 for b1 being full SubRelStr of L st b1 is bottom-inheriting & b1 is join-inheriting holds
b1 is finite-sups-inheriting
proof
let S be full SubRelStr of L; ::_thesis: ( S is bottom-inheriting & S is join-inheriting implies S is finite-sups-inheriting )
assume  ( S is bottom-inheriting & S is join-inheriting ) ; ::_thesis: S is finite-sups-inheriting
then reconsider S9 = S as full join-inheriting bottom-inheriting SubRelStr of L ;
let X be finite Subset of S; :: according to WAYBEL34:def_18 ::_thesis: ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S )
reconsider X9 = X as Subset of S9 ;
A1: X is finite ;
defpred S1[ set ] means  for Y being finite Subset of S9 st Y = L holds
( ex_sup_of Y,L & "\/" (Y,L) = sup Y );
A2: Bottom L = "\/" ({},L) ;
 Bottom S9 = "\/" ({},S9) ;
then A3: S1[ {} ] by A2, Th60, YELLOW_0:42;
A4: for x, B being set st x in X & B c= X & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in X & B c= X & S1[B] implies S1[B \/ {x}] )
assume that
 x in X and
 B c= X and
A5: for Y being finite Subset of S9 st Y = B holds
( ex_sup_of Y,L & "\/" (Y,L) = sup Y ) ; ::_thesis: S1[B \/ {x}]
let Y be finite Subset of S9; ::_thesis: ( Y = B \/ {x} implies ( ex_sup_of Y,L & "\/" (Y,L) = sup Y ) )
assume A6: Y = B \/ {x} ; ::_thesis: ( ex_sup_of Y,L & "\/" (Y,L) = sup Y )
A7: B c= Y by A6, XBOOLE_1:7;
A8: {x} c= Y by A6, XBOOLE_1:7;
reconsider Z = B as finite Subset of S9 by A7, XBOOLE_1:1;
A9: ex_sup_of Z,L by A5;
A10: "\/" (Z,L) = sup Z by A5;
 x in Y by A8, ZFMISC_1:31;
then reconsider x = x as Element of S9 ;
reconsider a = x as Element of L by YELLOW_0:58;
A11: ex_sup_of {a},L by YELLOW_0:38;
hence  ex_sup_of Y,L by A6, A9, YELLOW_2:3; ::_thesis: "\/" (Y,L) = sup Y
A12: ( Z = {} or ( Z <> {} & S9 is with_suprema ) ) ;
A13: ex_sup_of {x},S9 by YELLOW_0:54;
A14: ex_sup_of Z,S9 by A12, YELLOW_0:42, YELLOW_0:54;
thus  "\/" (Y,L) = ("\/" (Z,L)) "\/" (sup {a}) by A6, A9, A11, YELLOW_2:3
.= ("\/" (Z,L)) "\/" a by YELLOW_0:39
.= (sup Z) "\/" x by A10, YELLOW_0:70
.= (sup Z) "\/" (sup {x}) by YELLOW_0:39
.= sup Y by A6, A13, A14, YELLOW_2:3 ; ::_thesis: verum
end;
 S1[X] from FINSET_1:sch_2(A1, A3, A4);
then  "\/" (X,L) = sup X9 ;
hence  ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) ; ::_thesis: verum
end;
end;

theorem Th61: :: WAYBEL34:61
for S, T being non empty RelStr
for f being Function of S,T st f is finite-sups-preserving holds
( f is join-preserving & f is bottom-preserving )
proof
let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is finite-sups-preserving holds
( f is join-preserving & f is bottom-preserving )
let f be Function of S,T; ::_thesis: ( f is finite-sups-preserving implies ( f is join-preserving & f is bottom-preserving ) )
assume A1: for X being finite Subset of S holds f preserves_sup_of X ; :: according to WAYBEL34:def_15 ::_thesis: ( f is join-preserving & f is bottom-preserving )
thus  f is join-preserving ::_thesis: f is bottom-preserving
proof
let x, y be Element of S; :: according to WAYBEL_0:def_35 ::_thesis: f preserves_sup_of {x,y}
thus  f preserves_sup_of {x,y} by A1; ::_thesis: verum
end;
thus  f preserves_sup_of {} S by A1; :: according to WAYBEL34:def_16 ::_thesis: verum
end;

theorem Th62: :: WAYBEL34:62
for S, T being lower-bounded with_suprema Poset
for f being Function of S,T st f is join-preserving & f is bottom-preserving holds
f is finite-sups-preserving
proof
let S, T be lower-bounded with_suprema Poset; ::_thesis: for f being Function of S,T st f is join-preserving & f is bottom-preserving holds
f is finite-sups-preserving
let f be Function of S,T; ::_thesis: ( f is join-preserving & f is bottom-preserving implies f is finite-sups-preserving )
assume A1: ( f is join-preserving & f is bottom-preserving ) ; ::_thesis: f is finite-sups-preserving
let X be finite Subset of S; :: according to WAYBEL34:def_15 ::_thesis: f preserves_sup_of X
A2: X is finite ;
defpred S1[ set ] means  for Y being finite Subset of S st Y = $1 holds
f preserves_sup_of Y;
 f preserves_sup_of {} S by A1, Def16;
then A3: S1[ {} ] ;
A4: for x, B being set st x in X & B c= X & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in X & B c= X & S1[B] implies S1[B \/ {x}] )
assume that
 x in X and
 B c= X and
A5: for Y being finite Subset of S st Y = B holds
f preserves_sup_of Y ; ::_thesis: S1[B \/ {x}]
let Y be finite Subset of S; ::_thesis: ( Y = B \/ {x} implies f preserves_sup_of Y )
assume A6: Y = B \/ {x} ; ::_thesis: f preserves_sup_of Y
A7: B c= Y by A6, XBOOLE_1:7;
A8: {x} c= Y by A6, XBOOLE_1:7;
reconsider Z = B as finite Subset of S by A7, XBOOLE_1:1;
A9: x in Y by A8, ZFMISC_1:31;
then reconsider x = x as Element of S ;
A10: f preserves_sup_of Z by A5;
 ( f .: Z = {} or ( f .: Z <> {} & f .: Z is finite ) ) ;
then A11: ex_sup_of f .: Z,T by YELLOW_0:42, YELLOW_0:54;
A12: ex_sup_of {(f . x)},T by YELLOW_0:54;
 ( Z = {} or Z <> {} ) ;
then A13: ex_sup_of Z,S by YELLOW_0:42, YELLOW_0:54;
A14: f preserves_sup_of {(sup Z),x} by A1, WAYBEL_0:def_35;
A15: sup {x} = x by YELLOW_0:39;
A16: ex_sup_of {x},S by YELLOW_0:38;
A17: ex_sup_of Y,S by A9, YELLOW_0:54;
assume  ex_sup_of Y,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: Y,T & "\/" ((f .: Y),T) = f . ("\/" (Y,S)) )
thus  ex_sup_of f .: Y,T by A9, YELLOW_0:54; ::_thesis: "\/" ((f .: Y),T) = f . ("\/" (Y,S))
 dom f = the carrier of S by FUNCT_2:def_1;
then  Im (f,x) = {(f . x)} by FUNCT_1:59;
then A18: f .: Y = (f .: Z) \/ {(f . x)} by A6, RELAT_1:120;
 sup {(f . x)} = f . x by YELLOW_0:39;
hence  sup (f .: Y) = (sup (f .: Z)) "\/" (f . x) by A11, A12, A18, YELLOW_2:3
.= (f . (sup Z)) "\/" (f . x) by A10, A13, WAYBEL_0:def_31
.= f . ((sup Z) "\/" x) by A14, YELLOW_3:9
.= f . (sup Y) by A6, A13, A15, A16, A17, YELLOW_0:36 ;
::_thesis: verum
end;
 S1[X] from FINSET_1:sch_2(A2, A3, A4);
hence  f preserves_sup_of X ; ::_thesis: verum
end;

registration
let S, T be non empty RelStr ;
cluster Function-like quasi_total sups-preserving  ->  finite-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is sups-preserving holds
b1 is finite-sups-preserving
proof
let f be Function of S,T; ::_thesis: ( f is sups-preserving implies f is finite-sups-preserving )
assume  for X being Subset of S holds f preserves_sup_of X ; :: according to WAYBEL_0:def_33 ::_thesis: f is finite-sups-preserving
hence  for X being finite Subset of S holds f preserves_sup_of X ; :: according to WAYBEL34:def_15 ::_thesis: verum
end;
cluster Function-like quasi_total finite-sups-preserving  ->  join-preserving bottom-preserving for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is finite-sups-preserving holds
( b1 is join-preserving & b1 is bottom-preserving ) by Th61;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving finite-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st
( b1 is sups-preserving & b1 is finite-sups-preserving )
proof
set f = the sups-preserving Function of S,T;
take  the sups-preserving Function of S,T ; ::_thesis: ( the sups-preserving Function of S,T is sups-preserving & the sups-preserving Function of S,T is finite-sups-preserving )
thus  ( the sups-preserving Function of S,T is sups-preserving & the sups-preserving Function of S,T is finite-sups-preserving ) ; ::_thesis: verum
end;
end;

registration
let L be non empty lower-bounded Poset;
cluster CompactSublatt L ->  lower-bounded ;
coherence
 CompactSublatt L is lower-bounded
proof
 Bottom L is compact by WAYBEL_3:15;
then reconsider c = Bottom L as Element of (CompactSublatt L) by WAYBEL_8:def_1;
take  c ; :: according to YELLOW_0:def_4 ::_thesis: c is_<=_than the carrier of (CompactSublatt L)
let b be Element of (CompactSublatt L); :: according to LATTICE3:def_8 ::_thesis: ( not b in the carrier of (CompactSublatt L) or c <= b )
assume  b in the carrier of (CompactSublatt L) ; ::_thesis: c <= b
reconsider x = b as Element of L by YELLOW_0:58;
 Bottom L <= x by YELLOW_0:44;
hence  c <= b by YELLOW_0:60; ::_thesis: verum
end;
end;

theorem Th63: :: WAYBEL34:63
for S being RelStr
for T being non empty RelStr
for f being Function of S,T
for S9 being SubRelStr of S
for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
proof
let S be RelStr ; ::_thesis: for T being non empty RelStr
for f being Function of S,T
for S9 being SubRelStr of S
for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
let T be non empty RelStr ; ::_thesis: for f being Function of S,T
for S9 being SubRelStr of S
for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
let f be Function of S,T; ::_thesis: for S9 being SubRelStr of S
for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
let S9 be SubRelStr of S; ::_thesis: for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
let T9 be SubRelStr of T; ::_thesis: ( f .: the carrier of S9 c= the carrier of T9 implies f | the carrier of S9 is Function of S9,T9 )
assume A1: f .: the carrier of S9 c= the carrier of T9 ; ::_thesis: f | the carrier of S9 is Function of S9,T9
set g = f | the carrier of S9;
A2: dom f = the carrier of S by FUNCT_2:def_1;
 the carrier of S9 c= the carrier of S by YELLOW_0:def_13;
then A3: dom (f | the carrier of S9) = the carrier of S9 by A2, RELAT_1:62;
 rng (f | the carrier of S9) = f .: the carrier of S9 by RELAT_1:115;
hence  f | the carrier of S9 is Function of S9,T9 by A1, A3, FUNCT_2:2; ::_thesis: verum
end;

theorem Th64: :: WAYBEL34:64
for S, T being LATTICE
for f being join-preserving Function of S,T
for S9 being non empty full join-inheriting SubRelStr of S
for T9 being non empty full join-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
proof
let S, T be LATTICE; ::_thesis: for f being join-preserving Function of S,T
for S9 being non empty full join-inheriting SubRelStr of S
for T9 being non empty full join-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
let f be join-preserving Function of S,T; ::_thesis: for S9 being non empty full join-inheriting SubRelStr of S
for T9 being non empty full join-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
let S9 be non empty full join-inheriting SubRelStr of S; ::_thesis: for T9 being non empty full join-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
let T9 be non empty full join-inheriting SubRelStr of T; ::_thesis: for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
let g be Function of S9,T9; ::_thesis: ( g = f | the carrier of S9 implies g is join-preserving )
assume A1: g = f | the carrier of S9 ; ::_thesis: g is join-preserving
now__::_thesis:_for_x,_y_being_Element_of_S9_holds_g_._(x_"\/"_y)_=_(g_._x)_"\/"_(g_._y)
let x, y be Element of S9; ::_thesis: g . (x "\/" y) = (g . x) "\/" (g . y)
reconsider a = x, b = y as Element of S by YELLOW_0:58;
 x "\/" y = a "\/" b by YELLOW_0:70;
then A2: g . (x "\/" y) = f . (a "\/" b) by A1, FUNCT_1:49;
A3: g . x = f . a by A1, FUNCT_1:49;
A4: g . y = f . b by A1, FUNCT_1:49;
thus g . (x "\/" y) = (f . a) "\/" (f . b) by A2, WAYBEL_6:2
.= (g . x) "\/" (g . y) by A3, A4, YELLOW_0:70 ; ::_thesis: verum
end;
hence  g is join-preserving by WAYBEL_6:2; ::_thesis: verum
end;

theorem Th65: :: WAYBEL34:65
for S, T being lower-bounded LATTICE
for f being finite-sups-preserving Function of S,T
for S9 being non empty full finite-sups-inheriting SubRelStr of S
for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
proof
let S, T be lower-bounded LATTICE; ::_thesis: for f being finite-sups-preserving Function of S,T
for S9 being non empty full finite-sups-inheriting SubRelStr of S
for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
let f be finite-sups-preserving Function of S,T; ::_thesis: for S9 being non empty full finite-sups-inheriting SubRelStr of S
for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
let S9 be non empty full finite-sups-inheriting SubRelStr of S; ::_thesis: for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
let T9 be non empty full finite-sups-inheriting SubRelStr of T; ::_thesis: for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
let g be Function of S9,T9; ::_thesis: ( g = f | the carrier of S9 implies g is finite-sups-preserving )
assume A1: g = f | the carrier of S9 ; ::_thesis: g is finite-sups-preserving
 Bottom S9 = Bottom S by Th60;
then g . (Bottom S9) = f . (Bottom S) by A1, FUNCT_1:49
.= Bottom T by Def17
.= Bottom T9 by Th60 ;
then  g is bottom-preserving by Def17;
hence  g is finite-sups-preserving by A1, Th62, Th64; ::_thesis: verum
end;

registration
let L be complete LATTICE;
cluster CompactSublatt L ->  finite-sups-inheriting ;
coherence
 CompactSublatt L is finite-sups-inheriting
proof
 Bottom L in the carrier of (CompactSublatt L) by WAYBEL_8:3;
then  CompactSublatt L is non empty full join-inheriting bottom-inheriting SubRelStr of L by Def19;
hence  CompactSublatt L is finite-sups-inheriting ; ::_thesis: verum
end;
end;

theorem Th66: :: WAYBEL34:66
for S, T being complete LATTICE
for d being sups-preserving Function of T,S holds
( d is compact-preserving iff d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
proof
let S, T be complete LATTICE; ::_thesis: for d being sups-preserving Function of T,S holds
( d is compact-preserving iff d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
let d be sups-preserving Function of T,S; ::_thesis: ( d is compact-preserving iff d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
thus  ( d is compact-preserving implies d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ) ::_thesis: ( d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) implies d is compact-preserving )
proof
assume A1: for x being Element of T st x is compact holds
d . x is compact ; :: according to WAYBEL34:def_14 ::_thesis: d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S)
 d .: the carrier of (CompactSublatt T) c= the carrier of (CompactSublatt S)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in d .: the carrier of (CompactSublatt T) or y in the carrier of (CompactSublatt S) )
assume  y in d .: the carrier of (CompactSublatt T) ; ::_thesis: y in the carrier of (CompactSublatt S)
then consider x being set  such that
A2: x in the carrier of T and
A3: x in the carrier of (CompactSublatt T) and
A4: y = d . x by FUNCT_2:64;
reconsider x = x as Element of T by A2;
 x is compact by A3, WAYBEL_8:def_1;
then  d . x is compact by A1;
hence  y in the carrier of (CompactSublatt S) by A4, WAYBEL_8:def_1; ::_thesis: verum
end;
hence  d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) by Th63, Th65; ::_thesis: verum
end;
assume A5: d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ; ::_thesis: d is compact-preserving
let x be Element of T; :: according to WAYBEL34:def_14 ::_thesis: ( x is compact implies d . x is compact )
assume  x is compact ; ::_thesis: d . x is compact
then A6: x in the carrier of (CompactSublatt T) by WAYBEL_8:def_1;
then  d . x = (d | the carrier of (CompactSublatt T)) . x by FUNCT_1:49;
then  d . x in the carrier of (CompactSublatt S) by A5, A6, FUNCT_2:5;
hence  d . x is compact by WAYBEL_8:def_1; ::_thesis: verum
end;

theorem :: WAYBEL34:67
for S, T being complete LATTICE st T is algebraic holds
for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
proof
let S, T be complete LATTICE; ::_thesis: ( T is algebraic implies for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ) )
assume A1: T is algebraic ; ::_thesis: for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
let g be infs-preserving Function of S,T; ::_thesis: ( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
hereby  ::_thesis: ( (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) implies g is directed-sups-preserving )
assume  g is directed-sups-preserving ; ::_thesis: (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S)
then  LowerAdj g is waybelow-preserving by Th22;
then  LowerAdj g is compact-preserving by Th56;
hence  (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) by Th66; ::_thesis: verum
end;
assume  (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ; ::_thesis: g is directed-sups-preserving
then  LowerAdj g is compact-preserving by Th66;
then  LowerAdj g is waybelow-preserving by A1, Th57;
hence  g is directed-sups-preserving by A1, Th23; ::_thesis: verum
end;