:: WAYBEL_1 semantic presentation begin definition let L1, L2 be non empty 1-sorted ; let f be Function of L1,L2; :: original: one-to-one redefine attrf is one-to-one means :: WAYBEL_1:def 1 for x, y being Element of L1 st f . x = f . y holds x = y; compatibility ( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds x = y ) proof thus ( f is one-to-one implies for x, y being Element of L1 st f . x = f . y holds x = y ) by FUNCT_2:19; ::_thesis: ( ( for x, y being Element of L1 st f . x = f . y holds x = y ) implies f is one-to-one ) assume for x, y being Element of L1 st f . x = f . y holds x = y ; ::_thesis: f is one-to-one then for x, y being set st x in the carrier of L1 & y in the carrier of L1 & f . x = f . y holds x = y ; hence f is one-to-one by FUNCT_2:19; ::_thesis: verum end; end; :: deftheorem defines one-to-one WAYBEL_1:def_1_:_ for L1, L2 being non empty 1-sorted for f being Function of L1,L2 holds ( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds x = y ); definition let L1, L2 be non empty RelStr ; let f be Function of L1,L2; redefine attr f is monotone means :Def2: :: WAYBEL_1:def 2 for x, y being Element of L1 st x <= y holds f . x <= f . y; compatibility ( f is monotone iff for x, y being Element of L1 st x <= y holds f . x <= f . y ) proof thus ( f is monotone implies for x, y being Element of L1 st x <= y holds f . x <= f . y ) by ORDERS_3:def_5; ::_thesis: ( ( for x, y being Element of L1 st x <= y holds f . x <= f . y ) implies f is monotone ) assume for x, y being Element of L1 st x <= y holds f . x <= f . y ; ::_thesis: f is monotone hence for x, y being Element of L1 st x <= y holds for a, b being Element of L2 st a = f . x & b = f . y holds a <= b ; :: according to ORDERS_3:def_5 ::_thesis: verum end; end; :: deftheorem Def2 defines monotone WAYBEL_1:def_2_:_ for L1, L2 being non empty RelStr for f being Function of L1,L2 holds ( f is monotone iff for x, y being Element of L1 st x <= y holds f . x <= f . y ); theorem Th1: :: WAYBEL_1:1 for L being transitive antisymmetric with_infima RelStr for x, y, z being Element of L st x <= y holds x "/\" z <= y "/\" z proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for x, y, z being Element of L st x <= y holds x "/\" z <= y "/\" z let x, y, z be Element of L; ::_thesis: ( x <= y implies x "/\" z <= y "/\" z ) A1: x "/\" z <= x by YELLOW_0:23; A2: x "/\" z <= z by YELLOW_0:23; assume x <= y ; ::_thesis: x "/\" z <= y "/\" z then x "/\" z <= y by A1, ORDERS_2:3; hence x "/\" z <= y "/\" z by A2, YELLOW_0:23; ::_thesis: verum end; theorem Th2: :: WAYBEL_1:2 for L being transitive antisymmetric with_suprema RelStr for x, y, z being Element of L st x <= y holds x "\/" z <= y "\/" z proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for x, y, z being Element of L st x <= y holds x "\/" z <= y "\/" z let x, y, z be Element of L; ::_thesis: ( x <= y implies x "\/" z <= y "\/" z ) A1: y <= y "\/" z by YELLOW_0:22; A2: z <= y "\/" z by YELLOW_0:22; assume x <= y ; ::_thesis: x "\/" z <= y "\/" z then x <= y "\/" z by A1, ORDERS_2:3; hence x "\/" z <= y "\/" z by A2, YELLOW_0:22; ::_thesis: verum end; theorem Th3: :: WAYBEL_1:3 for L being non empty antisymmetric lower-bounded RelStr for x being Element of L holds ( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) ) proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for x being Element of L holds ( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) ) let x be Element of L; ::_thesis: ( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) ) thus ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) ::_thesis: ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) proof assume L is with_infima ; ::_thesis: (Bottom L) "/\" x = Bottom L then ( Bottom L <= (Bottom L) "/\" x & (Bottom L) "/\" x <= Bottom L ) by YELLOW_0:23, YELLOW_0:44; hence (Bottom L) "/\" x = Bottom L by ORDERS_2:2; ::_thesis: verum end; assume A1: L is with_suprema ; ::_thesis: ( not L is reflexive or not L is transitive or (Bottom L) "\/" x = x ) then A2: x <= (Bottom L) "\/" x by YELLOW_0:22; assume ( L is reflexive & L is transitive ) ; ::_thesis: (Bottom L) "\/" x = x then A3: x <= x by ORDERS_2:1; Bottom L <= x by YELLOW_0:44; then (Bottom L) "\/" x <= x by A1, A3, YELLOW_0:22; hence (Bottom L) "\/" x = x by A2, ORDERS_2:2; ::_thesis: verum end; theorem Th4: :: WAYBEL_1:4 for L being non empty antisymmetric upper-bounded RelStr for x being Element of L holds ( ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) & ( L is with_suprema implies (Top L) "\/" x = Top L ) ) proof let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: for x being Element of L holds ( ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) & ( L is with_suprema implies (Top L) "\/" x = Top L ) ) let x be Element of L; ::_thesis: ( ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) & ( L is with_suprema implies (Top L) "\/" x = Top L ) ) thus ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) ::_thesis: ( L is with_suprema implies (Top L) "\/" x = Top L ) proof assume A1: ( L is with_infima & L is transitive & L is reflexive ) ; ::_thesis: (Top L) "/\" x = x then x "/\" x <= (Top L) "/\" x by Th1, YELLOW_0:45; then A2: x <= (Top L) "/\" x by A1, YELLOW_0:25; (Top L) "/\" x <= x by A1, YELLOW_0:23; hence (Top L) "/\" x = x by A2, ORDERS_2:2; ::_thesis: verum end; assume L is with_suprema ; ::_thesis: (Top L) "\/" x = Top L then ( (Top L) "\/" x <= Top L & Top L <= (Top L) "\/" x ) by YELLOW_0:22, YELLOW_0:45; hence (Top L) "\/" x = Top L by ORDERS_2:2; ::_thesis: verum end; definition let L be non empty RelStr ; attrL is distributive means :Def3: :: WAYBEL_1:def 3 for x, y, z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z); end; :: deftheorem Def3 defines distributive WAYBEL_1:def_3_:_ for L being non empty RelStr holds ( L is distributive iff for x, y, z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ); theorem Th5: :: WAYBEL_1:5 for L being LATTICE holds ( L is distributive iff for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ) proof let L be LATTICE; ::_thesis: ( L is distributive iff for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ) hereby ::_thesis: ( ( for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ) implies L is distributive ) assume A1: L is distributive ; ::_thesis: for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) let x, y, z be Element of L; ::_thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) thus x "\/" (y "/\" z) = (x "\/" (z "/\" x)) "\/" (y "/\" z) by LATTICE3:17 .= x "\/" ((z "/\" x) "\/" (z "/\" y)) by LATTICE3:14 .= x "\/" ((x "\/" y) "/\" z) by A1, Def3 .= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" z) by LATTICE3:18 .= (x "\/" y) "/\" (x "\/" z) by A1, Def3 ; ::_thesis: verum end; assume A2: for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ; ::_thesis: L is distributive let x, y, z be Element of L; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) thus x "/\" (y "\/" z) = (x "/\" (x "\/" z)) "/\" (y "\/" z) by LATTICE3:18 .= x "/\" ((z "\/" x) "/\" (y "\/" z)) by LATTICE3:16 .= x "/\" (z "\/" (x "/\" y)) by A2 .= ((y "/\" x) "\/" x) "/\" ((x "/\" y) "\/" z) by LATTICE3:17 .= (x "/\" y) "\/" (x "/\" z) by A2 ; ::_thesis: verum end; registration let X be set ; cluster BoolePoset X -> distributive ; coherence BoolePoset X is distributive proof let x, y, z be Element of (BoolePoset X); :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) thus x "/\" (y "\/" z) = x /\ (y "\/" z) by YELLOW_1:17 .= x /\ (y \/ z) by YELLOW_1:17 .= (x /\ y) \/ (x /\ z) by XBOOLE_1:23 .= (x "/\" y) \/ (x /\ z) by YELLOW_1:17 .= (x "/\" y) \/ (x "/\" z) by YELLOW_1:17 .= (x "/\" y) "\/" (x "/\" z) by YELLOW_1:17 ; ::_thesis: verum end; end; definition let S be non empty RelStr ; let X be set ; pred ex_min_of X,S means :: WAYBEL_1:def 4 ( ex_inf_of X,S & "/\" (X,S) in X ); pred ex_max_of X,S means :Def5: :: WAYBEL_1:def 5 ( ex_sup_of X,S & "\/" (X,S) in X ); end; :: deftheorem defines ex_min_of WAYBEL_1:def_4_:_ for S being non empty RelStr for X being set holds ( ex_min_of X,S iff ( ex_inf_of X,S & "/\" (X,S) in X ) ); :: deftheorem Def5 defines ex_max_of WAYBEL_1:def_5_:_ for S being non empty RelStr for X being set holds ( ex_max_of X,S iff ( ex_sup_of X,S & "\/" (X,S) in X ) ); notation let S be non empty RelStr ; let X be set ; synonym X has_the_min_in S for ex_min_of X,S; synonym X has_the_max_in S for ex_max_of X,S; end; definition let S be non empty RelStr ; let s be Element of S; let X be set ; preds is_minimum_of X means :Def6: :: WAYBEL_1:def 6 ( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X ); preds is_maximum_of X means :Def7: :: WAYBEL_1:def 7 ( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X ); end; :: deftheorem Def6 defines is_minimum_of WAYBEL_1:def_6_:_ for S being non empty RelStr for s being Element of S for X being set holds ( s is_minimum_of X iff ( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X ) ); :: deftheorem Def7 defines is_maximum_of WAYBEL_1:def_7_:_ for S being non empty RelStr for s being Element of S for X being set holds ( s is_maximum_of X iff ( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X ) ); registration let L be RelStr ; cluster id L -> isomorphic ; coherence id L is isomorphic proof percases ( not L is empty or L is empty ) ; supposeA1: not L is empty ; ::_thesis: id L is isomorphic A2: id L = (id L) " by FUNCT_1:45; id L is monotone by A1, YELLOW_2:11; hence id L is isomorphic by A1, A2, WAYBEL_0:def_38; ::_thesis: verum end; suppose L is empty ; ::_thesis: id L is isomorphic hence id L is isomorphic by WAYBEL_0:def_38; ::_thesis: verum end; end; end; end; definition let L1, L2 be RelStr ; predL1,L2 are_isomorphic means :Def8: :: WAYBEL_1:def 8 ex f being Function of L1,L2 st f is isomorphic ; reflexivity for L1 being RelStr ex f being Function of L1,L1 st f is isomorphic proof let L be RelStr ; ::_thesis: ex f being Function of L,L st f is isomorphic take id L ; ::_thesis: id L is isomorphic thus id L is isomorphic ; ::_thesis: verum end; end; :: deftheorem Def8 defines are_isomorphic WAYBEL_1:def_8_:_ for L1, L2 being RelStr holds ( L1,L2 are_isomorphic iff ex f being Function of L1,L2 st f is isomorphic ); theorem :: WAYBEL_1:6 for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds L2,L1 are_isomorphic proof let L1, L2 be non empty RelStr ; ::_thesis: ( L1,L2 are_isomorphic implies L2,L1 are_isomorphic ) given f being Function of L1,L2 such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: L2,L1 are_isomorphic consider g being Function of L2,L1 such that A2: g = f " and A3: g is monotone by A1, WAYBEL_0:def_38; f = g " by A1, A2, FUNCT_1:43; then g is isomorphic by A1, A2, A3, WAYBEL_0:def_38; hence L2,L1 are_isomorphic by Def8; ::_thesis: verum end; theorem :: WAYBEL_1:7 for L1, L2, L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds L1,L3 are_isomorphic proof let L1, L2, L3 be RelStr ; ::_thesis: ( L1,L2 are_isomorphic & L2,L3 are_isomorphic implies L1,L3 are_isomorphic ) given f1 being Function of L1,L2 such that A1: f1 is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not L2,L3 are_isomorphic or L1,L3 are_isomorphic ) given f2 being Function of L2,L3 such that A2: f2 is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: L1,L3 are_isomorphic A3: now__::_thesis:_(_L1_is_empty_implies_f2_*_f1_is_Function_of_L1,L3_) assume L1 is empty ; ::_thesis: f2 * f1 is Function of L1,L3 then the carrier of L1 is empty ; hence f2 * f1 is Function of L1,L3 by FUNCT_2:13; ::_thesis: verum end; percases ( ( not L1 is empty & not L2 is empty & not L3 is empty ) or L1 is empty or L2 is empty or L3 is empty ) ; suppose ( not L1 is empty & not L2 is empty & not L3 is empty ) ; ::_thesis: L1,L3 are_isomorphic then reconsider L1 = L1, L2 = L2, L3 = L3 as non empty RelStr ; reconsider f1 = f1 as Function of L1,L2 ; reconsider f2 = f2 as Function of L2,L3 ; consider g1 being Function of L2,L1 such that A4: ( g1 = f1 " & g1 is monotone ) by A1, WAYBEL_0:def_38; consider g2 being Function of L3,L2 such that A5: ( g2 = f2 " & g2 is monotone ) by A2, WAYBEL_0:def_38; A6: f2 * f1 is monotone by A1, A2, YELLOW_2:12; ( g1 * g2 is monotone & g1 * g2 = (f2 * f1) " ) by A1, A2, A4, A5, FUNCT_1:44, YELLOW_2:12; then f2 * f1 is isomorphic by A1, A2, A6, WAYBEL_0:def_38; hence L1,L3 are_isomorphic by Def8; ::_thesis: verum end; supposeA7: L1 is empty ; ::_thesis: L1,L3 are_isomorphic then reconsider f = f2 * f1 as Function of L1,L3 by A3; L2 is empty by A1, A7, WAYBEL_0:def_38; then L3 is empty by A2, WAYBEL_0:def_38; then f is isomorphic by A7, WAYBEL_0:def_38; hence L1,L3 are_isomorphic by Def8; ::_thesis: verum end; supposeA8: L2 is empty ; ::_thesis: L1,L3 are_isomorphic then reconsider f = f2 * f1 as Function of L1,L3 by A1, A3, WAYBEL_0:def_38; ( L1 is empty & L3 is empty ) by A1, A2, A8, WAYBEL_0:def_38; then f is isomorphic by WAYBEL_0:def_38; hence L1,L3 are_isomorphic by Def8; ::_thesis: verum end; supposeA9: L3 is empty ; ::_thesis: L1,L3 are_isomorphic then A10: L2 is empty by A2, WAYBEL_0:def_38; then reconsider f = f2 * f1 as Function of L1,L3 by A1, A3, WAYBEL_0:def_38; L1 is empty by A1, A10, WAYBEL_0:def_38; then f is isomorphic by A9, WAYBEL_0:def_38; hence L1,L3 are_isomorphic by Def8; ::_thesis: verum end; end; end; begin definition let S, T be RelStr ; mode Connection of S,T -> set means :Def9: :: WAYBEL_1:def 9 ex g being Function of S,T ex d being Function of T,S st it = [g,d]; existence ex b1 being set ex g being Function of S,T ex d being Function of T,S st b1 = [g,d] proof set g = the Function of S,T; set d = the Function of T,S; take [ the Function of S,T, the Function of T,S] ; ::_thesis: ex g being Function of S,T ex d being Function of T,S st [ the Function of S,T, the Function of T,S] = [g,d] thus ex g being Function of S,T ex d being Function of T,S st [ the Function of S,T, the Function of T,S] = [g,d] ; ::_thesis: verum end; end; :: deftheorem Def9 defines Connection WAYBEL_1:def_9_:_ for S, T being RelStr for b3 being set holds ( b3 is Connection of S,T iff ex g being Function of S,T ex d being Function of T,S st b3 = [g,d] ); definition let S, T be RelStr ; let g be Function of S,T; let d be Function of T,S; :: original: [ redefine func[g,d] -> Connection of S,T; coherence [g,d] is Connection of S,T by Def9; end; definition let S, T be non empty RelStr ; let gc be Connection of S,T; attrgc is Galois means :Def10: :: WAYBEL_1:def 10 ex g being Function of S,T ex d being Function of T,S st ( gc = [g,d] & g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) ); end; :: deftheorem Def10 defines Galois WAYBEL_1:def_10_:_ for S, T being non empty RelStr for gc being Connection of S,T holds ( gc is Galois iff ex g being Function of S,T ex d being Function of T,S st ( gc = [g,d] & g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) ) ); theorem Th8: :: WAYBEL_1:8 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S holds ( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) ) ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S holds ( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) ) ) let g be Function of S,T; ::_thesis: for d being Function of T,S holds ( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) ) ) let d be Function of T,S; ::_thesis: ( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) ) ) hereby ::_thesis: ( g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) implies [g,d] is Galois ) assume [g,d] is Galois ; ::_thesis: ( g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) ) then consider g9 being Function of S,T, d9 being Function of T,S such that A1: [g,d] = [g9,d9] and A2: ( g9 is monotone & d9 is monotone & ( for t being Element of T for s being Element of S holds ( t <= g9 . s iff d9 . t <= s ) ) ) by Def10; ( g = g9 & d = d9 ) by A1, XTUPLE_0:1; hence ( g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) ) by A2; ::_thesis: verum end; thus ( g is monotone & d is monotone & ( for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) ) implies [g,d] is Galois ) by Def10; ::_thesis: verum end; definition let S, T be non empty RelStr ; let g be Function of S,T; attrg is upper_adjoint means :Def11: :: WAYBEL_1:def 11 ex d being Function of T,S st [g,d] is Galois ; end; :: deftheorem Def11 defines upper_adjoint WAYBEL_1:def_11_:_ for S, T being non empty RelStr for g being Function of S,T holds ( g is upper_adjoint iff ex d being Function of T,S st [g,d] is Galois ); definition let S, T be non empty RelStr ; let d be Function of T,S; attrd is lower_adjoint means :Def12: :: WAYBEL_1:def 12 ex g being Function of S,T st [g,d] is Galois ; end; :: deftheorem Def12 defines lower_adjoint WAYBEL_1:def_12_:_ for S, T being non empty RelStr for d being Function of T,S holds ( d is lower_adjoint iff ex g being Function of S,T st [g,d] is Galois ); theorem Th9: :: WAYBEL_1:9 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st [g,d] is Galois holds ( g is upper_adjoint & d is lower_adjoint ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st [g,d] is Galois holds ( g is upper_adjoint & d is lower_adjoint ) let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois holds ( g is upper_adjoint & d is lower_adjoint ) let d be Function of T,S; ::_thesis: ( [g,d] is Galois implies ( g is upper_adjoint & d is lower_adjoint ) ) assume A1: [g,d] is Galois ; ::_thesis: ( g is upper_adjoint & d is lower_adjoint ) hence ex d being Function of T,S st [g,d] is Galois ; :: according to WAYBEL_1:def_11 ::_thesis: d is lower_adjoint thus ex g being Function of S,T st [g,d] is Galois by A1; :: according to WAYBEL_1:def_12 ::_thesis: verum end; theorem Th10: :: WAYBEL_1:10 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S holds ( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S holds ( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) ) let g be Function of S,T; ::_thesis: for d being Function of T,S holds ( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) ) let d be Function of T,S; ::_thesis: ( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) ) hereby ::_thesis: ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) implies [g,d] is Galois ) assume A1: [g,d] is Galois ; ::_thesis: ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) hence g is monotone by Th8; ::_thesis: for t being Element of T holds d . t is_minimum_of g " (uparrow t) let t be Element of T; ::_thesis: d . t is_minimum_of g " (uparrow t) thus d . t is_minimum_of g " (uparrow t) ::_thesis: verum proof set X = g " (uparrow t); t <= g . (d . t) by A1, Th8; then g . (d . t) in uparrow t by WAYBEL_0:18; then A2: d . t in g " (uparrow t) by FUNCT_2:38; then A3: for s being Element of S st s is_<=_than g " (uparrow t) holds d . t >= s by LATTICE3:def_8; A4: d . t is_<=_than g " (uparrow t) proof let s be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not s in g " (uparrow t) or d . t <= s ) assume s in g " (uparrow t) ; ::_thesis: d . t <= s then g . s in uparrow t by FUNCT_1:def_7; then t <= g . s by WAYBEL_0:18; hence d . t <= s by A1, Th8; ::_thesis: verum end; hence ( ex_inf_of g " (uparrow t),S & d . t = inf (g " (uparrow t)) ) by A3, YELLOW_0:31; :: according to WAYBEL_1:def_6 ::_thesis: "/\" ((g " (uparrow t)),S) in g " (uparrow t) thus "/\" ((g " (uparrow t)),S) in g " (uparrow t) by A4, A2, A3, YELLOW_0:31; ::_thesis: verum end; end; assume that A5: g is monotone and A6: for t being Element of T holds d . t is_minimum_of g " (uparrow t) ; ::_thesis: [g,d] is Galois A7: for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) proof let t be Element of T; ::_thesis: for s being Element of S holds ( t <= g . s iff d . t <= s ) let s be Element of S; ::_thesis: ( t <= g . s iff d . t <= s ) set X = g " (uparrow t); hereby ::_thesis: ( d . t <= s implies t <= g . s ) assume t <= g . s ; ::_thesis: d . t <= s then g . s in uparrow t by WAYBEL_0:18; then A8: s in g " (uparrow t) by FUNCT_2:38; A9: d . t is_minimum_of g " (uparrow t) by A6; then ex_inf_of g " (uparrow t),S by Def6; then g " (uparrow t) is_>=_than inf (g " (uparrow t)) by YELLOW_0:def_10; then s >= inf (g " (uparrow t)) by A8, LATTICE3:def_8; hence d . t <= s by A9, Def6; ::_thesis: verum end; A10: d . t is_minimum_of g " (uparrow t) by A6; then inf (g " (uparrow t)) in g " (uparrow t) by Def6; then g . (inf (g " (uparrow t))) in uparrow t by FUNCT_1:def_7; then g . (inf (g " (uparrow t))) >= t by WAYBEL_0:18; then A11: g . (d . t) >= t by A10, Def6; assume d . t <= s ; ::_thesis: t <= g . s then g . (d . t) <= g . s by A5, Def2; hence t <= g . s by A11, ORDERS_2:3; ::_thesis: verum end; d is monotone proof let t1, t2 be Element of T; :: according to WAYBEL_1:def_2 ::_thesis: ( t1 <= t2 implies d . t1 <= d . t2 ) assume t1 <= t2 ; ::_thesis: d . t1 <= d . t2 then A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22; A13: d . t2 is_minimum_of g " (uparrow t2) by A6; then A14: ex_inf_of g " (uparrow t2),S by Def6; A15: d . t1 is_minimum_of g " (uparrow t1) by A6; then ex_inf_of g " (uparrow t1),S by Def6; then inf (g " (uparrow t1)) <= inf (g " (uparrow t2)) by A14, A12, RELAT_1:143, YELLOW_0:35; then d . t1 <= inf (g " (uparrow t2)) by A15, Def6; hence d . t1 <= d . t2 by A13, Def6; ::_thesis: verum end; hence [g,d] is Galois by A5, A7, Th8; ::_thesis: verum end; theorem Th11: :: WAYBEL_1:11 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S holds ( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S holds ( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) ) let g be Function of S,T; ::_thesis: for d being Function of T,S holds ( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) ) let d be Function of T,S; ::_thesis: ( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) ) hereby ::_thesis: ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) implies [g,d] is Galois ) assume A1: [g,d] is Galois ; ::_thesis: ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) hence d is monotone by Th8; ::_thesis: for s being Element of S holds g . s is_maximum_of d " (downarrow s) let s be Element of S; ::_thesis: g . s is_maximum_of d " (downarrow s) thus g . s is_maximum_of d " (downarrow s) ::_thesis: verum proof set X = d " (downarrow s); s >= d . (g . s) by A1, Th8; then d . (g . s) in downarrow s by WAYBEL_0:17; then A2: g . s in d " (downarrow s) by FUNCT_2:38; then A3: for t being Element of T st t is_>=_than d " (downarrow s) holds g . s <= t by LATTICE3:def_9; A4: g . s is_>=_than d " (downarrow s) proof let t be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not t in d " (downarrow s) or t <= g . s ) assume t in d " (downarrow s) ; ::_thesis: t <= g . s then d . t in downarrow s by FUNCT_1:def_7; then s >= d . t by WAYBEL_0:17; hence t <= g . s by A1, Th8; ::_thesis: verum end; hence ( ex_sup_of d " (downarrow s),T & g . s = sup (d " (downarrow s)) ) by A3, YELLOW_0:30; :: according to WAYBEL_1:def_7 ::_thesis: "\/" ((d " (downarrow s)),T) in d " (downarrow s) thus "\/" ((d " (downarrow s)),T) in d " (downarrow s) by A4, A2, A3, YELLOW_0:30; ::_thesis: verum end; end; assume that A5: d is monotone and A6: for s being Element of S holds g . s is_maximum_of d " (downarrow s) ; ::_thesis: [g,d] is Galois A7: for t being Element of T for s being Element of S holds ( s >= d . t iff g . s >= t ) proof let t be Element of T; ::_thesis: for s being Element of S holds ( s >= d . t iff g . s >= t ) let s be Element of S; ::_thesis: ( s >= d . t iff g . s >= t ) set X = d " (downarrow s); A8: g . s is_maximum_of d " (downarrow s) by A6; then sup (d " (downarrow s)) in d " (downarrow s) by Def7; then d . (sup (d " (downarrow s))) in downarrow s by FUNCT_1:def_7; then d . (sup (d " (downarrow s))) <= s by WAYBEL_0:17; then A9: d . (g . s) <= s by A8, Def7; hereby ::_thesis: ( g . s >= t implies s >= d . t ) assume s >= d . t ; ::_thesis: g . s >= t then d . t in downarrow s by WAYBEL_0:17; then A10: t in d " (downarrow s) by FUNCT_2:38; ex_sup_of d " (downarrow s),T by A8, Def7; then d " (downarrow s) is_<=_than sup (d " (downarrow s)) by YELLOW_0:def_9; then t <= sup (d " (downarrow s)) by A10, LATTICE3:def_9; hence g . s >= t by A8, Def7; ::_thesis: verum end; assume g . s >= t ; ::_thesis: s >= d . t then d . (g . s) >= d . t by A5, Def2; hence s >= d . t by A9, ORDERS_2:3; ::_thesis: verum end; g is monotone proof let s1, s2 be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies g . s1 <= g . s2 ) assume s1 <= s2 ; ::_thesis: g . s1 <= g . s2 then A11: downarrow s1 c= downarrow s2 by WAYBEL_0:21; A12: g . s2 is_maximum_of d " (downarrow s2) by A6; then A13: ex_sup_of d " (downarrow s2),T by Def7; A14: g . s1 is_maximum_of d " (downarrow s1) by A6; then ex_sup_of d " (downarrow s1),T by Def7; then sup (d " (downarrow s1)) <= sup (d " (downarrow s2)) by A13, A11, RELAT_1:143, YELLOW_0:34; then g . s1 <= sup (d " (downarrow s2)) by A14, Def7; hence g . s1 <= g . s2 by A12, Def7; ::_thesis: verum end; hence [g,d] is Galois by A5, A7, Th8; ::_thesis: verum end; theorem Th12: :: WAYBEL_1:12 for S, T being non empty Poset for g being Function of S,T st g is upper_adjoint holds g is infs-preserving proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T st g is upper_adjoint holds g is infs-preserving let g be Function of S,T; ::_thesis: ( g is upper_adjoint implies g is infs-preserving ) given d being Function of T,S such that A1: [g,d] is Galois ; :: according to WAYBEL_1:def_11 ::_thesis: g is infs-preserving let X be Subset of S; :: according to WAYBEL_0:def_32 ::_thesis: g preserves_inf_of X set s = inf X; assume A2: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of g .: X,T & "/\" ((g .: X),T) = g . ("/\" (X,S)) ) A3: for t being Element of T st t is_<=_than g .: X holds g . (inf X) >= t proof let t be Element of T; ::_thesis: ( t is_<=_than g .: X implies g . (inf X) >= t ) assume A4: t is_<=_than g .: X ; ::_thesis: g . (inf X) >= t d . t is_<=_than X proof let si be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not si in X or d . t <= si ) assume si in X ; ::_thesis: d . t <= si then g . si in g .: X by FUNCT_2:35; then t <= g . si by A4, LATTICE3:def_8; hence d . t <= si by A1, Th8; ::_thesis: verum end; then d . t <= inf X by A2, YELLOW_0:31; hence g . (inf X) >= t by A1, Th8; ::_thesis: verum end; g . (inf X) is_<=_than g .: X proof let t be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not t in g .: X or g . (inf X) <= t ) assume t in g .: X ; ::_thesis: g . (inf X) <= t then consider si being Element of S such that A5: si in X and A6: t = g . si by FUNCT_2:65; A7: g is monotone by A1, Th8; reconsider si = si as Element of S ; inf X is_<=_than X by A2, YELLOW_0:31; then inf X <= si by A5, LATTICE3:def_8; hence g . (inf X) <= t by A7, A6, Def2; ::_thesis: verum end; hence ( ex_inf_of g .: X,T & "/\" ((g .: X),T) = g . ("/\" (X,S)) ) by A3, YELLOW_0:31; ::_thesis: verum end; registration let S, T be non empty Poset; cluster Function-like quasi_total upper_adjoint -> infs-preserving for M2( bool [: the carrier of S, the carrier of T:]); coherence for b1 being Function of S,T st b1 is upper_adjoint holds b1 is infs-preserving by Th12; end; theorem Th13: :: WAYBEL_1:13 for S, T being non empty Poset for d being Function of T,S st d is lower_adjoint holds d is sups-preserving proof let S, T be non empty Poset; ::_thesis: for d being Function of T,S st d is lower_adjoint holds d is sups-preserving let d be Function of T,S; ::_thesis: ( d is lower_adjoint implies d is sups-preserving ) given g being Function of S,T such that A1: [g,d] is Galois ; :: according to WAYBEL_1:def_12 ::_thesis: d is sups-preserving let X be Subset of T; :: according to WAYBEL_0:def_33 ::_thesis: d preserves_sup_of X set t = sup X; assume A2: ex_sup_of X,T ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of d .: X,S & "\/" ((d .: X),S) = d . ("\/" (X,T)) ) A3: for s being Element of S st s is_>=_than d .: X holds d . (sup X) <= s proof let s be Element of S; ::_thesis: ( s is_>=_than d .: X implies d . (sup X) <= s ) assume A4: s is_>=_than d .: X ; ::_thesis: d . (sup X) <= s g . s is_>=_than X proof let ti be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not ti in X or ti <= g . s ) assume ti in X ; ::_thesis: ti <= g . s then d . ti in d .: X by FUNCT_2:35; then s >= d . ti by A4, LATTICE3:def_9; hence ti <= g . s by A1, Th8; ::_thesis: verum end; then g . s >= sup X by A2, YELLOW_0:30; hence d . (sup X) <= s by A1, Th8; ::_thesis: verum end; d . (sup X) is_>=_than d .: X proof let s be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not s in d .: X or s <= d . (sup X) ) assume s in d .: X ; ::_thesis: s <= d . (sup X) then consider ti being Element of T such that A5: ti in X and A6: s = d . ti by FUNCT_2:65; A7: d is monotone by A1, Th8; reconsider ti = ti as Element of T ; sup X is_>=_than X by A2, YELLOW_0:30; then sup X >= ti by A5, LATTICE3:def_9; hence s <= d . (sup X) by A7, A6, Def2; ::_thesis: verum end; hence ( ex_sup_of d .: X,S & "\/" ((d .: X),S) = d . ("\/" (X,T)) ) by A3, YELLOW_0:30; ::_thesis: verum end; registration let S, T be non empty Poset; cluster Function-like quasi_total lower_adjoint -> sups-preserving for M2( bool [: the carrier of S, the carrier of T:]); coherence for b1 being Function of S,T st b1 is lower_adjoint holds b1 is sups-preserving by Th13; end; theorem Th14: :: WAYBEL_1:14 for S, T being non empty Poset for g being Function of S,T st S is complete & g is infs-preserving holds ex d being Function of T,S st ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T st S is complete & g is infs-preserving holds ex d being Function of T,S st ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) let g be Function of S,T; ::_thesis: ( S is complete & g is infs-preserving implies ex d being Function of T,S st ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) ) assume that A1: S is complete and A2: g is infs-preserving ; ::_thesis: ex d being Function of T,S st ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) defpred S1[ set , set ] means ex t being Element of T st ( t = $1 & $2 = inf (g " (uparrow t)) ); A3: for e being set st e in the carrier of T holds ex u being set st ( u in the carrier of S & S1[e,u] ) proof let e be set ; ::_thesis: ( e in the carrier of T implies ex u being set st ( u in the carrier of S & S1[e,u] ) ) assume e in the carrier of T ; ::_thesis: ex u being set st ( u in the carrier of S & S1[e,u] ) then reconsider t = e as Element of T ; take inf (g " (uparrow t)) ; ::_thesis: ( inf (g " (uparrow t)) in the carrier of S & S1[e, inf (g " (uparrow t))] ) thus ( inf (g " (uparrow t)) in the carrier of S & S1[e, inf (g " (uparrow t))] ) ; ::_thesis: verum end; consider d being Function of the carrier of T, the carrier of S such that A4: for e being set st e in the carrier of T holds S1[e,d . e] from FUNCT_2:sch_1(A3); A5: for t being Element of T holds d . t = inf (g " (uparrow t)) proof let t be Element of T; ::_thesis: d . t = inf (g " (uparrow t)) ex t1 being Element of T st ( t1 = t & d . t = inf (g " (uparrow t1)) ) by A4; hence d . t = inf (g " (uparrow t)) ; ::_thesis: verum end; reconsider d = d as Function of T,S ; for X being Filter of S holds g preserves_inf_of X by A2, WAYBEL_0:def_32; then A6: g is monotone by WAYBEL_0:69; A7: for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) proof let t be Element of T; ::_thesis: for s being Element of S holds ( t <= g . s iff d . t <= s ) let s be Element of S; ::_thesis: ( t <= g . s iff d . t <= s ) A8: ex_inf_of uparrow t,T by WAYBEL_0:39; A9: ex_inf_of g " (uparrow t),S by A1, YELLOW_0:17; then inf (g " (uparrow t)) is_<=_than g " (uparrow t) by YELLOW_0:31; then A10: d . t is_<=_than g " (uparrow t) by A5; hereby ::_thesis: ( d . t <= s implies t <= g . s ) assume t <= g . s ; ::_thesis: d . t <= s then g . s in uparrow t by WAYBEL_0:18; then s in g " (uparrow t) by FUNCT_2:38; hence d . t <= s by A10, LATTICE3:def_8; ::_thesis: verum end; g preserves_inf_of g " (uparrow t) by A2, WAYBEL_0:def_32; then ( ex_inf_of g .: (g " (uparrow t)),T & g . (inf (g " (uparrow t))) = inf (g .: (g " (uparrow t))) ) by A9, WAYBEL_0:def_30; then g . (inf (g " (uparrow t))) >= inf (uparrow t) by A8, FUNCT_1:75, YELLOW_0:35; then A11: g . (inf (g " (uparrow t))) >= t by WAYBEL_0:39; assume d . t <= s ; ::_thesis: t <= g . s then g . (d . t) <= g . s by A6, Def2; then g . (inf (g " (uparrow t))) <= g . s by A5; hence t <= g . s by A11, ORDERS_2:3; ::_thesis: verum end; take d ; ::_thesis: ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) d is monotone proof let t1, t2 be Element of T; :: according to WAYBEL_1:def_2 ::_thesis: ( t1 <= t2 implies d . t1 <= d . t2 ) assume t1 <= t2 ; ::_thesis: d . t1 <= d . t2 then A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22; ( ex_inf_of g " (uparrow t1),S & ex_inf_of g " (uparrow t2),S ) by A1, YELLOW_0:17; then inf (g " (uparrow t1)) <= inf (g " (uparrow t2)) by A12, RELAT_1:143, YELLOW_0:35; then d . t1 <= inf (g " (uparrow t2)) by A5; hence d . t1 <= d . t2 by A5; ::_thesis: verum end; hence [g,d] is Galois by A6, A7, Th8; ::_thesis: for t being Element of T holds d . t is_minimum_of g " (uparrow t) let t be Element of T; ::_thesis: d . t is_minimum_of g " (uparrow t) thus A13: ex_inf_of g " (uparrow t),S by A1, YELLOW_0:17; :: according to WAYBEL_1:def_6 ::_thesis: ( d . t = "/\" ((g " (uparrow t)),S) & "/\" ((g " (uparrow t)),S) in g " (uparrow t) ) thus A14: d . t = inf (g " (uparrow t)) by A5; ::_thesis: "/\" ((g " (uparrow t)),S) in g " (uparrow t) A15: ex_inf_of uparrow t,T by WAYBEL_0:39; g preserves_inf_of g " (uparrow t) by A2, WAYBEL_0:def_32; then ( ex_inf_of g .: (g " (uparrow t)),T & g . (inf (g " (uparrow t))) = inf (g .: (g " (uparrow t))) ) by A13, WAYBEL_0:def_30; then g . (inf (g " (uparrow t))) >= inf (uparrow t) by A15, FUNCT_1:75, YELLOW_0:35; then g . (inf (g " (uparrow t))) >= t by WAYBEL_0:39; then g . (d . t) >= t by A5; then g . (d . t) in uparrow t by WAYBEL_0:18; hence "/\" ((g " (uparrow t)),S) in g " (uparrow t) by A14, FUNCT_2:38; ::_thesis: verum end; theorem Th15: :: WAYBEL_1:15 for S, T being non empty Poset for d being Function of T,S st T is complete & d is sups-preserving holds ex g being Function of S,T st ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) proof let S, T be non empty Poset; ::_thesis: for d being Function of T,S st T is complete & d is sups-preserving holds ex g being Function of S,T st ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) let d be Function of T,S; ::_thesis: ( T is complete & d is sups-preserving implies ex g being Function of S,T st ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) ) assume that A1: T is complete and A2: d is sups-preserving ; ::_thesis: ex g being Function of S,T st ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) defpred S1[ set , set ] means ex s being Element of S st ( s = $1 & $2 = sup (d " (downarrow s)) ); A3: for e being set st e in the carrier of S holds ex u being set st ( u in the carrier of T & S1[e,u] ) proof let e be set ; ::_thesis: ( e in the carrier of S implies ex u being set st ( u in the carrier of T & S1[e,u] ) ) assume e in the carrier of S ; ::_thesis: ex u being set st ( u in the carrier of T & S1[e,u] ) then reconsider s = e as Element of S ; take sup (d " (downarrow s)) ; ::_thesis: ( sup (d " (downarrow s)) in the carrier of T & S1[e, sup (d " (downarrow s))] ) thus ( sup (d " (downarrow s)) in the carrier of T & S1[e, sup (d " (downarrow s))] ) ; ::_thesis: verum end; consider g being Function of the carrier of S, the carrier of T such that A4: for e being set st e in the carrier of S holds S1[e,g . e] from FUNCT_2:sch_1(A3); A5: for s being Element of S holds g . s = sup (d " (downarrow s)) proof let s be Element of S; ::_thesis: g . s = sup (d " (downarrow s)) ex s1 being Element of S st ( s1 = s & g . s = sup (d " (downarrow s1)) ) by A4; hence g . s = sup (d " (downarrow s)) ; ::_thesis: verum end; reconsider g = g as Function of S,T ; for X being Ideal of T holds d preserves_sup_of X by A2, WAYBEL_0:def_33; then A6: d is monotone by WAYBEL_0:72; A7: for t being Element of T for s being Element of S holds ( s >= d . t iff g . s >= t ) proof let t be Element of T; ::_thesis: for s being Element of S holds ( s >= d . t iff g . s >= t ) let s be Element of S; ::_thesis: ( s >= d . t iff g . s >= t ) A8: ex_sup_of downarrow s,S by WAYBEL_0:34; A9: ex_sup_of d " (downarrow s),T by A1, YELLOW_0:17; then sup (d " (downarrow s)) is_>=_than d " (downarrow s) by YELLOW_0:30; then A10: g . s is_>=_than d " (downarrow s) by A5; hereby ::_thesis: ( g . s >= t implies s >= d . t ) assume s >= d . t ; ::_thesis: g . s >= t then d . t in downarrow s by WAYBEL_0:17; then t in d " (downarrow s) by FUNCT_2:38; hence g . s >= t by A10, LATTICE3:def_9; ::_thesis: verum end; d preserves_sup_of d " (downarrow s) by A2, WAYBEL_0:def_33; then ( ex_sup_of d .: (d " (downarrow s)),S & d . (sup (d " (downarrow s))) = sup (d .: (d " (downarrow s))) ) by A9, WAYBEL_0:def_31; then d . (sup (d " (downarrow s))) <= sup (downarrow s) by A8, FUNCT_1:75, YELLOW_0:34; then A11: d . (sup (d " (downarrow s))) <= s by WAYBEL_0:34; assume g . s >= t ; ::_thesis: s >= d . t then d . (g . s) >= d . t by A6, Def2; then d . (sup (d " (downarrow s))) >= d . t by A5; hence s >= d . t by A11, ORDERS_2:3; ::_thesis: verum end; take g ; ::_thesis: ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) g is monotone proof let s1, s2 be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies g . s1 <= g . s2 ) assume s1 <= s2 ; ::_thesis: g . s1 <= g . s2 then A12: downarrow s1 c= downarrow s2 by WAYBEL_0:21; ( ex_sup_of d " (downarrow s1),T & ex_sup_of d " (downarrow s2),T ) by A1, YELLOW_0:17; then sup (d " (downarrow s1)) <= sup (d " (downarrow s2)) by A12, RELAT_1:143, YELLOW_0:34; then g . s1 <= sup (d " (downarrow s2)) by A5; hence g . s1 <= g . s2 by A5; ::_thesis: verum end; hence [g,d] is Galois by A6, A7, Th8; ::_thesis: for s being Element of S holds g . s is_maximum_of d " (downarrow s) let s be Element of S; ::_thesis: g . s is_maximum_of d " (downarrow s) thus A13: ex_sup_of d " (downarrow s),T by A1, YELLOW_0:17; :: according to WAYBEL_1:def_7 ::_thesis: ( g . s = "\/" ((d " (downarrow s)),T) & "\/" ((d " (downarrow s)),T) in d " (downarrow s) ) thus A14: g . s = sup (d " (downarrow s)) by A5; ::_thesis: "\/" ((d " (downarrow s)),T) in d " (downarrow s) A15: ex_sup_of downarrow s,S by WAYBEL_0:34; d preserves_sup_of d " (downarrow s) by A2, WAYBEL_0:def_33; then ( ex_sup_of d .: (d " (downarrow s)),S & d . (sup (d " (downarrow s))) = sup (d .: (d " (downarrow s))) ) by A13, WAYBEL_0:def_31; then d . (sup (d " (downarrow s))) <= sup (downarrow s) by A15, FUNCT_1:75, YELLOW_0:34; then d . (sup (d " (downarrow s))) <= s by WAYBEL_0:34; then d . (g . s) <= s by A5; then d . (g . s) in downarrow s by WAYBEL_0:17; hence "\/" ((d " (downarrow s)),T) in d " (downarrow s) by A14, FUNCT_2:38; ::_thesis: verum end; theorem :: WAYBEL_1:16 for S, T being non empty Poset for g being Function of S,T st S is complete holds ( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T st S is complete holds ( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) ) let g be Function of S,T; ::_thesis: ( S is complete implies ( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) ) ) assume A1: S is complete ; ::_thesis: ( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) ) hereby ::_thesis: ( g is monotone & g is upper_adjoint implies g is infs-preserving ) assume g is infs-preserving ; ::_thesis: ( g is monotone & g is upper_adjoint ) then ex d being Function of T,S st ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) by A1, Th14; hence ( g is monotone & g is upper_adjoint ) by Def11, Th10; ::_thesis: verum end; assume g is monotone ; ::_thesis: ( not g is upper_adjoint or g is infs-preserving ) assume ex d being Function of T,S st [g,d] is Galois ; :: according to WAYBEL_1:def_11 ::_thesis: g is infs-preserving then g is upper_adjoint by Def11; hence g is infs-preserving ; ::_thesis: verum end; theorem Th17: :: WAYBEL_1:17 for S, T being non empty Poset for d being Function of T,S st T is complete holds ( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) ) proof let S, T be non empty Poset; ::_thesis: for d being Function of T,S st T is complete holds ( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) ) let d be Function of T,S; ::_thesis: ( T is complete implies ( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) ) ) assume A1: T is complete ; ::_thesis: ( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) ) hereby ::_thesis: ( d is monotone & d is lower_adjoint implies d is sups-preserving ) assume d is sups-preserving ; ::_thesis: ( d is monotone & d is lower_adjoint ) then ex g being Function of S,T st ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) by A1, Th15; hence ( d is monotone & d is lower_adjoint ) by Def12, Th11; ::_thesis: verum end; assume d is monotone ; ::_thesis: ( not d is lower_adjoint or d is sups-preserving ) assume ex g being Function of S,T st [g,d] is Galois ; :: according to WAYBEL_1:def_12 ::_thesis: d is sups-preserving then d is lower_adjoint by Def12; hence d is sups-preserving ; ::_thesis: verum end; theorem Th18: :: WAYBEL_1:18 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st [g,d] is Galois holds ( d * g <= id S & id T <= g * d ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st [g,d] is Galois holds ( d * g <= id S & id T <= g * d ) let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois holds ( d * g <= id S & id T <= g * d ) let d be Function of T,S; ::_thesis: ( [g,d] is Galois implies ( d * g <= id S & id T <= g * d ) ) assume A1: [g,d] is Galois ; ::_thesis: ( d * g <= id S & id T <= g * d ) for s being Element of S holds (d * g) . s <= (id S) . s proof let s be Element of S; ::_thesis: (d * g) . s <= (id S) . s d . (g . s) <= s by A1, Th8; then (d * g) . s <= s by FUNCT_2:15; hence (d * g) . s <= (id S) . s by FUNCT_1:18; ::_thesis: verum end; hence d * g <= id S by YELLOW_2:9; ::_thesis: id T <= g * d for t being Element of T holds (id T) . t <= (g * d) . t proof let t be Element of T; ::_thesis: (id T) . t <= (g * d) . t t <= g . (d . t) by A1, Th8; then t <= (g * d) . t by FUNCT_2:15; hence (id T) . t <= (g * d) . t by FUNCT_1:18; ::_thesis: verum end; hence id T <= g * d by YELLOW_2:9; ::_thesis: verum end; theorem Th19: :: WAYBEL_1:19 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds [g,d] is Galois proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds [g,d] is Galois let g be Function of S,T; ::_thesis: for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds [g,d] is Galois let d be Function of T,S; ::_thesis: ( g is monotone & d is monotone & d * g <= id S & id T <= g * d implies [g,d] is Galois ) assume that A1: g is monotone and A2: d is monotone and A3: d * g <= id S and A4: id T <= g * d ; ::_thesis: [g,d] is Galois for t being Element of T for s being Element of S holds ( t <= g . s iff d . t <= s ) proof let t be Element of T; ::_thesis: for s being Element of S holds ( t <= g . s iff d . t <= s ) let s be Element of S; ::_thesis: ( t <= g . s iff d . t <= s ) hereby ::_thesis: ( d . t <= s implies t <= g . s ) (d * g) . s <= (id S) . s by A3, YELLOW_2:9; then d . (g . s) <= (id S) . s by FUNCT_2:15; then A5: d . (g . s) <= s by FUNCT_1:18; assume t <= g . s ; ::_thesis: d . t <= s then d . t <= d . (g . s) by A2, Def2; hence d . t <= s by A5, ORDERS_2:3; ::_thesis: verum end; (id T) . t <= (g * d) . t by A4, YELLOW_2:9; then (id T) . t <= g . (d . t) by FUNCT_2:15; then A6: t <= g . (d . t) by FUNCT_1:18; assume d . t <= s ; ::_thesis: t <= g . s then g . (d . t) <= g . s by A1, Def2; hence t <= g . s by A6, ORDERS_2:3; ::_thesis: verum end; hence [g,d] is Galois by A1, A2, Th8; ::_thesis: verum end; theorem Th20: :: WAYBEL_1:20 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds ( d = (d * g) * d & g = (g * d) * g ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds ( d = (d * g) * d & g = (g * d) * g ) let g be Function of S,T; ::_thesis: for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds ( d = (d * g) * d & g = (g * d) * g ) let d be Function of T,S; ::_thesis: ( g is monotone & d is monotone & d * g <= id S & id T <= g * d implies ( d = (d * g) * d & g = (g * d) * g ) ) assume that A1: g is monotone and A2: d is monotone and A3: d * g <= id S and A4: id T <= g * d ; ::_thesis: ( d = (d * g) * d & g = (g * d) * g ) for t being Element of T holds d . t = ((d * g) * d) . t proof let t be Element of T; ::_thesis: d . t = ((d * g) * d) . t (id T) . t <= (g * d) . t by A4, YELLOW_2:9; then t <= (g * d) . t by FUNCT_1:18; then d . t <= d . ((g * d) . t) by A2, Def2; then d . t <= (d * (g * d)) . t by FUNCT_2:15; then A5: d . t <= ((d * g) * d) . t by RELAT_1:36; (d * g) . (d . t) <= (id S) . (d . t) by A3, YELLOW_2:9; then (d * g) . (d . t) <= d . t by FUNCT_1:18; then d . t >= ((d * g) * d) . t by FUNCT_2:15; hence d . t = ((d * g) * d) . t by A5, ORDERS_2:2; ::_thesis: verum end; hence d = (d * g) * d by FUNCT_2:63; ::_thesis: g = (g * d) * g for s being Element of S holds g . s = ((g * d) * g) . s proof let s be Element of S; ::_thesis: g . s = ((g * d) * g) . s (d * g) . s <= (id S) . s by A3, YELLOW_2:9; then (d * g) . s <= s by FUNCT_1:18; then g . ((d * g) . s) <= g . s by A1, Def2; then (g * (d * g)) . s <= g . s by FUNCT_2:15; then A6: g . s >= ((g * d) * g) . s by RELAT_1:36; (id T) . (g . s) <= (g * d) . (g . s) by A4, YELLOW_2:9; then g . s <= (g * d) . (g . s) by FUNCT_1:18; then g . s <= ((g * d) * g) . s by FUNCT_2:15; hence g . s = ((g * d) * g) . s by A6, ORDERS_2:2; ::_thesis: verum end; hence g = (g * d) * g by FUNCT_2:63; ::_thesis: verum end; theorem Th21: :: WAYBEL_1:21 for S, T being non empty RelStr for g being Function of S,T for d being Function of T,S st g = (g * d) * g holds g * d is idempotent proof let S, T be non empty RelStr ; ::_thesis: for g being Function of S,T for d being Function of T,S st g = (g * d) * g holds g * d is idempotent let g be Function of S,T; ::_thesis: for d being Function of T,S st g = (g * d) * g holds g * d is idempotent let d be Function of T,S; ::_thesis: ( g = (g * d) * g implies g * d is idempotent ) assume g = (g * d) * g ; ::_thesis: g * d is idempotent hence (g * d) * (g * d) = g * d by RELAT_1:36; :: according to QUANTAL1:def_9 ::_thesis: verum end; theorem Th22: :: WAYBEL_1:22 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st [g,d] is Galois & g is onto holds for t being Element of T holds d . t is_minimum_of g " {t} proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st [g,d] is Galois & g is onto holds for t being Element of T holds d . t is_minimum_of g " {t} let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois & g is onto holds for t being Element of T holds d . t is_minimum_of g " {t} let d be Function of T,S; ::_thesis: ( [g,d] is Galois & g is onto implies for t being Element of T holds d . t is_minimum_of g " {t} ) assume that A1: [g,d] is Galois and A2: g is onto ; ::_thesis: for t being Element of T holds d . t is_minimum_of g " {t} A3: g is monotone by A1, Th8; let t be Element of T; ::_thesis: d . t is_minimum_of g " {t} A4: rng g = the carrier of T by A2, FUNCT_2:def_3; then A5: g .: (g " (uparrow t)) = uparrow t by FUNCT_1:77; A6: d . t is_minimum_of g " (uparrow t) by A1, Th10; then A7: d . t = inf (g " (uparrow t)) by Def6; then d . t in g " (uparrow t) by A6, Def6; then g . (d . t) in g .: (g " (uparrow t)) by FUNCT_2:35; then A8: t <= g . (d . t) by A5, WAYBEL_0:18; ex_inf_of g " (uparrow t),S by A6, Def6; then A9: d . t is_<=_than g " (uparrow t) by A7, YELLOW_0:31; consider s being set such that A10: s in the carrier of S and A11: g . s = t by A4, FUNCT_2:11; reconsider s = s as Element of S by A10; A12: t in {t} by TARSKI:def_1; A13: {t} c= uparrow {t} by WAYBEL_0:16; then s in g " (uparrow t) by A11, A12, FUNCT_2:38; then d . t <= s by A9, LATTICE3:def_8; then g . (d . t) <= t by A11, A3, Def2; then A14: g . (d . t) = t by A8, ORDERS_2:2; then A15: d . t in g " {t} by A12, FUNCT_2:38; A16: g " {t} c= g " (uparrow t) by RELAT_1:143, WAYBEL_0:16; thus A17: ex_inf_of g " {t},S :: according to WAYBEL_1:def_6 ::_thesis: ( d . t = "/\" ((g " {t}),S) & "/\" ((g " {t}),S) in g " {t} ) proof take d . t ; :: according to YELLOW_0:def_8 ::_thesis: ( d . t is_<=_than g " {t} & ( for b1 being M2( the carrier of S) holds ( not b1 is_<=_than g " {t} or b1 <= d . t ) ) & ( for b1 being M2( the carrier of S) holds ( not b1 is_<=_than g " {t} or ex b2 being M2( the carrier of S) st ( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t ) ) ) thus g " {t} is_>=_than d . t by A9, A16, YELLOW_0:9; ::_thesis: ( ( for b1 being M2( the carrier of S) holds ( not b1 is_<=_than g " {t} or b1 <= d . t ) ) & ( for b1 being M2( the carrier of S) holds ( not b1 is_<=_than g " {t} or ex b2 being M2( the carrier of S) st ( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t ) ) ) thus for b being Element of S st g " {t} is_>=_than b holds b <= d . t by A15, LATTICE3:def_8; ::_thesis: for b1 being M2( the carrier of S) holds ( not b1 is_<=_than g " {t} or ex b2 being M2( the carrier of S) st ( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t ) let c be Element of S; ::_thesis: ( not c is_<=_than g " {t} or ex b1 being M2( the carrier of S) st ( b1 is_<=_than g " {t} & not b1 <= c ) or c = d . t ) assume g " {t} is_>=_than c ; ::_thesis: ( ex b1 being M2( the carrier of S) st ( b1 is_<=_than g " {t} & not b1 <= c ) or c = d . t ) then A18: c <= d . t by A15, LATTICE3:def_8; assume for b being Element of S st g " {t} is_>=_than b holds b <= c ; ::_thesis: c = d . t then d . t <= c by A9, A16, YELLOW_0:9; hence c = d . t by A18, ORDERS_2:2; ::_thesis: verum end; then inf (g " {t}) is_<=_than g " {t} by YELLOW_0:31; then A19: inf (g " {t}) <= d . t by A15, LATTICE3:def_8; ex_inf_of g " (uparrow t),S by A6, Def6; then inf (g " {t}) >= d . t by A7, A13, A17, RELAT_1:143, YELLOW_0:35; hence d . t = inf (g " {t}) by A19, ORDERS_2:2; ::_thesis: "/\" ((g " {t}),S) in g " {t} hence "/\" ((g " {t}),S) in g " {t} by A12, A14, FUNCT_2:38; ::_thesis: verum end; theorem Th23: :: WAYBEL_1:23 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds g * d = id T proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds g * d = id T let g be Function of S,T; ::_thesis: for d being Function of T,S st ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds g * d = id T let d be Function of T,S; ::_thesis: ( ( for t being Element of T holds d . t is_minimum_of g " {t} ) implies g * d = id T ) assume A1: for t being Element of T holds d . t is_minimum_of g " {t} ; ::_thesis: g * d = id T for t being Element of T holds (g * d) . t = t proof let t be Element of T; ::_thesis: (g * d) . t = t d . t is_minimum_of g " {t} by A1; then ( d . t = inf (g " {t}) & inf (g " {t}) in g " {t} ) by Def6; then g . (d . t) in {t} by FUNCT_2:38; then g . (d . t) = t by TARSKI:def_1; hence (g * d) . t = t by FUNCT_2:15; ::_thesis: verum end; hence g * d = id T by FUNCT_2:124; ::_thesis: verum end; theorem :: WAYBEL_1:24 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st [g,d] is Galois holds ( g is onto iff d is V13() ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st [g,d] is Galois holds ( g is onto iff d is V13() ) let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois holds ( g is onto iff d is V13() ) let d be Function of T,S; ::_thesis: ( [g,d] is Galois implies ( g is onto iff d is V13() ) ) A1: ( the carrier of T = dom d & the carrier of T = dom (g * d) ) by FUNCT_2:def_1; assume A2: [g,d] is Galois ; ::_thesis: ( g is onto iff d is V13() ) then A3: ( d * g <= id S & id T <= g * d ) by Th18; hereby ::_thesis: ( d is V13() implies g is onto ) assume g is onto ; ::_thesis: d is V13() then for t being Element of T holds d . t is_minimum_of g " {t} by A2, Th22; then g * d = id T by Th23; hence d is V13() by FUNCT_2:23; ::_thesis: verum end; A4: rng (g * d) c= the carrier of T ; ( g is monotone & d is monotone ) by A2, Th8; then A5: d = (d * g) * d by A3, Th20 .= d * (g * d) by RELAT_1:36 ; assume d is V13() ; ::_thesis: g is onto then g * d = id T by A1, A4, A5, FUNCT_1:28; hence g is onto by FUNCT_2:23; ::_thesis: verum end; theorem Th25: :: WAYBEL_1:25 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st [g,d] is Galois & d is onto holds for s being Element of S holds g . s is_maximum_of d " {s} proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st [g,d] is Galois & d is onto holds for s being Element of S holds g . s is_maximum_of d " {s} let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois & d is onto holds for s being Element of S holds g . s is_maximum_of d " {s} let d be Function of T,S; ::_thesis: ( [g,d] is Galois & d is onto implies for s being Element of S holds g . s is_maximum_of d " {s} ) assume that A1: [g,d] is Galois and A2: d is onto ; ::_thesis: for s being Element of S holds g . s is_maximum_of d " {s} A3: d is monotone by A1, Th8; let s be Element of S; ::_thesis: g . s is_maximum_of d " {s} A4: rng d = the carrier of S by A2, FUNCT_2:def_3; then A5: d .: (d " (downarrow s)) = downarrow s by FUNCT_1:77; A6: g . s is_maximum_of d " (downarrow s) by A1, Th11; then A7: g . s = sup (d " (downarrow s)) by Def7; then g . s in d " (downarrow s) by A6, Def7; then d . (g . s) in d .: (d " (downarrow s)) by FUNCT_2:35; then A8: s >= d . (g . s) by A5, WAYBEL_0:17; ex_sup_of d " (downarrow s),T by A6, Def7; then A9: g . s is_>=_than d " (downarrow s) by A7, YELLOW_0:30; consider t being set such that A10: t in the carrier of T and A11: d . t = s by A4, FUNCT_2:11; reconsider t = t as Element of T by A10; A12: s in {s} by TARSKI:def_1; A13: {s} c= downarrow {s} by WAYBEL_0:16; then t in d " (downarrow s) by A11, A12, FUNCT_2:38; then g . s >= t by A9, LATTICE3:def_9; then d . (g . s) >= s by A11, A3, Def2; then A14: d . (g . s) = s by A8, ORDERS_2:2; then A15: g . s in d " {s} by A12, FUNCT_2:38; A16: d " {s} c= d " (downarrow s) by RELAT_1:143, WAYBEL_0:16; thus A17: ex_sup_of d " {s},T :: according to WAYBEL_1:def_7 ::_thesis: ( g . s = "\/" ((d " {s}),T) & "\/" ((d " {s}),T) in d " {s} ) proof take g . s ; :: according to YELLOW_0:def_7 ::_thesis: ( d " {s} is_<=_than g . s & ( for b1 being M2( the carrier of T) holds ( not d " {s} is_<=_than b1 or g . s <= b1 ) ) & ( for b1 being M2( the carrier of T) holds ( not d " {s} is_<=_than b1 or ex b2 being M2( the carrier of T) st ( d " {s} is_<=_than b2 & not b1 <= b2 ) or b1 = g . s ) ) ) thus d " {s} is_<=_than g . s by A9, A16, YELLOW_0:9; ::_thesis: ( ( for b1 being M2( the carrier of T) holds ( not d " {s} is_<=_than b1 or g . s <= b1 ) ) & ( for b1 being M2( the carrier of T) holds ( not d " {s} is_<=_than b1 or ex b2 being M2( the carrier of T) st ( d " {s} is_<=_than b2 & not b1 <= b2 ) or b1 = g . s ) ) ) thus for b being Element of T st d " {s} is_<=_than b holds b >= g . s by A15, LATTICE3:def_9; ::_thesis: for b1 being M2( the carrier of T) holds ( not d " {s} is_<=_than b1 or ex b2 being M2( the carrier of T) st ( d " {s} is_<=_than b2 & not b1 <= b2 ) or b1 = g . s ) let c be Element of T; ::_thesis: ( not d " {s} is_<=_than c or ex b1 being M2( the carrier of T) st ( d " {s} is_<=_than b1 & not c <= b1 ) or c = g . s ) assume d " {s} is_<=_than c ; ::_thesis: ( ex b1 being M2( the carrier of T) st ( d " {s} is_<=_than b1 & not c <= b1 ) or c = g . s ) then A18: c >= g . s by A15, LATTICE3:def_9; assume for b being Element of T st d " {s} is_<=_than b holds b >= c ; ::_thesis: c = g . s then g . s >= c by A9, A16, YELLOW_0:9; hence c = g . s by A18, ORDERS_2:2; ::_thesis: verum end; then sup (d " {s}) is_>=_than d " {s} by YELLOW_0:30; then A19: sup (d " {s}) >= g . s by A15, LATTICE3:def_9; ex_sup_of d " (downarrow s),T by A6, Def7; then sup (d " {s}) <= g . s by A7, A13, A17, RELAT_1:143, YELLOW_0:34; hence g . s = sup (d " {s}) by A19, ORDERS_2:2; ::_thesis: "\/" ((d " {s}),T) in d " {s} hence "\/" ((d " {s}),T) in d " {s} by A12, A14, FUNCT_2:38; ::_thesis: verum end; theorem Th26: :: WAYBEL_1:26 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds d * g = id S proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds d * g = id S let g be Function of S,T; ::_thesis: for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds d * g = id S let d be Function of T,S; ::_thesis: ( ( for s being Element of S holds g . s is_maximum_of d " {s} ) implies d * g = id S ) assume A1: for s being Element of S holds g . s is_maximum_of d " {s} ; ::_thesis: d * g = id S for s being Element of S holds (d * g) . s = s proof let s be Element of S; ::_thesis: (d * g) . s = s g . s is_maximum_of d " {s} by A1; then ( g . s = sup (d " {s}) & sup (d " {s}) in d " {s} ) by Def7; then d . (g . s) in {s} by FUNCT_2:38; then d . (g . s) = s by TARSKI:def_1; hence (d * g) . s = s by FUNCT_2:15; ::_thesis: verum end; hence d * g = id S by FUNCT_2:124; ::_thesis: verum end; theorem :: WAYBEL_1:27 for S, T being non empty Poset for g being Function of S,T for d being Function of T,S st [g,d] is Galois holds ( g is V13() iff d is onto ) proof let S, T be non empty Poset; ::_thesis: for g being Function of S,T for d being Function of T,S st [g,d] is Galois holds ( g is V13() iff d is onto ) let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois holds ( g is V13() iff d is onto ) let d be Function of T,S; ::_thesis: ( [g,d] is Galois implies ( g is V13() iff d is onto ) ) assume A1: [g,d] is Galois ; ::_thesis: ( g is V13() iff d is onto ) hereby ::_thesis: ( d is onto implies g is V13() ) A2: ( d * g <= id S & id T <= g * d ) by A1, Th18; ( g is monotone & d is monotone ) by A1, Th8; then A3: g = (g * d) * g by A2, Th20 .= g * (d * g) by RELAT_1:36 ; A4: ( the carrier of S = dom g & the carrier of S = dom (d * g) ) by FUNCT_2:def_1; A5: rng (d * g) c= the carrier of S ; assume g is V13() ; ::_thesis: d is onto then d * g = id S by A4, A5, A3, FUNCT_1:28; hence d is onto by FUNCT_2:23; ::_thesis: verum end; assume d is onto ; ::_thesis: g is V13() then for s being Element of S holds g . s is_maximum_of d " {s} by A1, Th25; then d * g = id S by Th26; hence g is V13() by FUNCT_2:23; ::_thesis: verum end; definition let L be non empty RelStr ; let p be Function of L,L; attrp is projection means :Def13: :: WAYBEL_1:def 13 ( p is idempotent & p is monotone ); end; :: deftheorem Def13 defines projection WAYBEL_1:def_13_:_ for L being non empty RelStr for p being Function of L,L holds ( p is projection iff ( p is idempotent & p is monotone ) ); registration let L be non empty RelStr ; cluster id L -> projection ; coherence id L is projection proof thus id L is idempotent by YELLOW_2:21; :: according to WAYBEL_1:def_13 ::_thesis: id L is monotone thus id L is monotone ; ::_thesis: verum end; end; registration let L be non empty RelStr ; cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total projection for M2( bool [: the carrier of L, the carrier of L:]); existence ex b1 being Function of L,L st b1 is projection proof take id L ; ::_thesis: id L is projection thus id L is projection ; ::_thesis: verum end; end; definition let L be non empty RelStr ; let c be Function of L,L; attrc is closure means :Def14: :: WAYBEL_1:def 14 ( c is projection & id L <= c ); end; :: deftheorem Def14 defines closure WAYBEL_1:def_14_:_ for L being non empty RelStr for c being Function of L,L holds ( c is closure iff ( c is projection & id L <= c ) ); registration let L be non empty RelStr ; cluster Function-like quasi_total closure -> projection for M2( bool [: the carrier of L, the carrier of L:]); coherence for b1 being Function of L,L st b1 is closure holds b1 is projection by Def14; end; Lm1: for L1, L2 being non empty RelStr for f being Function of L1,L2 st L2 is reflexive holds f <= f proof let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 st L2 is reflexive holds f <= f let f be Function of L1,L2; ::_thesis: ( L2 is reflexive implies f <= f ) assume L2 is reflexive ; ::_thesis: f <= f then for x being Element of L1 holds f . x <= f . x by ORDERS_2:1; hence f <= f by YELLOW_2:9; ::_thesis: verum end; registration let L be non empty reflexive RelStr ; cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total closure for M2( bool [: the carrier of L, the carrier of L:]); existence ex b1 being Function of L,L st b1 is closure proof take id L ; ::_thesis: id L is closure thus id L is projection ; :: according to WAYBEL_1:def_14 ::_thesis: id L <= id L thus id L <= id L by Lm1; ::_thesis: verum end; end; registration let L be non empty reflexive RelStr ; cluster id L -> closure ; coherence id L is closure proof thus id L is projection ; :: according to WAYBEL_1:def_14 ::_thesis: id L <= id L thus id L <= id L by Lm1; ::_thesis: verum end; end; definition let L be non empty RelStr ; let k be Function of L,L; attrk is kernel means :Def15: :: WAYBEL_1:def 15 ( k is projection & k <= id L ); end; :: deftheorem Def15 defines kernel WAYBEL_1:def_15_:_ for L being non empty RelStr for k being Function of L,L holds ( k is kernel iff ( k is projection & k <= id L ) ); registration let L be non empty RelStr ; cluster Function-like quasi_total kernel -> projection for M2( bool [: the carrier of L, the carrier of L:]); coherence for b1 being Function of L,L st b1 is kernel holds b1 is projection by Def15; end; registration let L be non empty reflexive RelStr ; cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total kernel for M2( bool [: the carrier of L, the carrier of L:]); existence ex b1 being Function of L,L st b1 is kernel proof take id L ; ::_thesis: id L is kernel thus id L is projection ; :: according to WAYBEL_1:def_15 ::_thesis: id L <= id L thus id L <= id L by Lm1; ::_thesis: verum end; end; registration let L be non empty reflexive RelStr ; cluster id L -> kernel ; coherence id L is kernel proof thus id L is projection ; :: according to WAYBEL_1:def_15 ::_thesis: id L <= id L thus id L <= id L by Lm1; ::_thesis: verum end; end; Lm2: for L being non empty 1-sorted for p being Function of L,L st p is idempotent holds for x being set st x in rng p holds p . x = x proof let L be non empty 1-sorted ; ::_thesis: for p being Function of L,L st p is idempotent holds for x being set st x in rng p holds p . x = x let p be Function of L,L; ::_thesis: ( p is idempotent implies for x being set st x in rng p holds p . x = x ) assume A1: p is idempotent ; ::_thesis: for x being set st x in rng p holds p . x = x let x be set ; ::_thesis: ( x in rng p implies p . x = x ) assume x in rng p ; ::_thesis: p . x = x then ex a being set st ( a in dom p & x = p . a ) by FUNCT_1:def_3; hence p . x = x by A1, YELLOW_2:18; ::_thesis: verum end; theorem Th28: :: WAYBEL_1:28 for L being non empty Poset for c being Function of L,L for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds inf X = c . (inf X) proof let L be non empty Poset; ::_thesis: for c being Function of L,L for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds inf X = c . (inf X) let c be Function of L,L; ::_thesis: for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds inf X = c . (inf X) let X be Subset of L; ::_thesis: ( c is closure & ex_inf_of X,L & X c= rng c implies inf X = c . (inf X) ) assume that A1: c is projection and A2: id L <= c and A3: ex_inf_of X,L and A4: X c= rng c ; :: according to WAYBEL_1:def_14 ::_thesis: inf X = c . (inf X) A5: c is monotone by A1, Def13; A6: c is idempotent by A1, Def13; c . (inf X) is_<=_than X proof let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X or c . (inf X) <= x ) assume A7: x in X ; ::_thesis: c . (inf X) <= x inf X is_<=_than X by A3, YELLOW_0:31; then inf X <= x by A7, LATTICE3:def_8; then c . (inf X) <= c . x by A5, Def2; hence c . (inf X) <= x by A4, A6, A7, Lm2; ::_thesis: verum end; then A8: c . (inf X) <= inf X by A3, YELLOW_0:31; (id L) . (inf X) <= c . (inf X) by A2, YELLOW_2:9; then inf X <= c . (inf X) by FUNCT_1:18; hence inf X = c . (inf X) by A8, ORDERS_2:2; ::_thesis: verum end; theorem Th29: :: WAYBEL_1:29 for L being non empty Poset for k being Function of L,L for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds sup X = k . (sup X) proof let L be non empty Poset; ::_thesis: for k being Function of L,L for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds sup X = k . (sup X) let k be Function of L,L; ::_thesis: for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds sup X = k . (sup X) let X be Subset of L; ::_thesis: ( k is kernel & ex_sup_of X,L & X c= rng k implies sup X = k . (sup X) ) assume that A1: k is projection and A2: k <= id L and A3: ex_sup_of X,L and A4: X c= rng k ; :: according to WAYBEL_1:def_15 ::_thesis: sup X = k . (sup X) A5: k is monotone by A1, Def13; A6: k is idempotent by A1, Def13; k . (sup X) is_>=_than X proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= k . (sup X) ) assume A7: x in X ; ::_thesis: x <= k . (sup X) sup X is_>=_than X by A3, YELLOW_0:30; then sup X >= x by A7, LATTICE3:def_9; then k . (sup X) >= k . x by A5, Def2; hence x <= k . (sup X) by A4, A6, A7, Lm2; ::_thesis: verum end; then A8: k . (sup X) >= sup X by A3, YELLOW_0:30; (id L) . (sup X) >= k . (sup X) by A2, YELLOW_2:9; then sup X >= k . (sup X) by FUNCT_1:18; hence sup X = k . (sup X) by A8, ORDERS_2:2; ::_thesis: verum end; definition let L1, L2 be non empty RelStr ; let g be Function of L1,L2; func corestr g -> Function of L1,(Image g) equals :: WAYBEL_1:def 16 the carrier of (Image g) |` g; coherence the carrier of (Image g) |` g is Function of L1,(Image g) proof A1: the carrier of L1 = dom g by FUNCT_2:def_1; A2: the carrier of (Image g) = rng g by YELLOW_0:def_15; then the carrier of (Image g) |` g = g by RELAT_1:94; hence the carrier of (Image g) |` g is Function of L1,(Image g) by A2, A1, FUNCT_2:1; ::_thesis: verum end; end; :: deftheorem defines corestr WAYBEL_1:def_16_:_ for L1, L2 being non empty RelStr for g being Function of L1,L2 holds corestr g = the carrier of (Image g) |` g; theorem Th30: :: WAYBEL_1:30 for L1, L2 being non empty RelStr for g being Function of L1,L2 holds corestr g = g proof let L1, L2 be non empty RelStr ; ::_thesis: for g being Function of L1,L2 holds corestr g = g let g be Function of L1,L2; ::_thesis: corestr g = g the carrier of (Image g) = rng g by YELLOW_0:def_15; hence corestr g = g by RELAT_1:94; ::_thesis: verum end; Lm3: for L1, L2 being non empty RelStr for g being Function of L1,L2 holds corestr g is onto proof let L1, L2 be non empty RelStr ; ::_thesis: for g being Function of L1,L2 holds corestr g is onto let g be Function of L1,L2; ::_thesis: corestr g is onto the carrier of (Image g) = rng g by YELLOW_0:def_15 .= rng (corestr g) by Th30 ; hence corestr g is onto by FUNCT_2:def_3; ::_thesis: verum end; registration let L1, L2 be non empty RelStr ; let g be Function of L1,L2; cluster corestr g -> onto ; coherence corestr g is onto by Lm3; end; theorem Th31: :: WAYBEL_1:31 for L1, L2 being non empty RelStr for g being Function of L1,L2 st g is monotone holds corestr g is monotone proof let L1, L2 be non empty RelStr ; ::_thesis: for g being Function of L1,L2 st g is monotone holds corestr g is monotone let g be Function of L1,L2; ::_thesis: ( g is monotone implies corestr g is monotone ) assume A1: g is monotone ; ::_thesis: corestr g is monotone let s1, s2 be Element of L1; :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies (corestr g) . s1 <= (corestr g) . s2 ) assume s1 <= s2 ; ::_thesis: (corestr g) . s1 <= (corestr g) . s2 then A2: g . s1 <= g . s2 by A1, Def2; reconsider s19 = g . s1, s29 = g . s2 as Element of L2 ; ( s19 = (corestr g) . s1 & s29 = (corestr g) . s2 ) by Th30; hence (corestr g) . s1 <= (corestr g) . s2 by A2, YELLOW_0:60; ::_thesis: verum end; definition let L1, L2 be non empty RelStr ; let g be Function of L1,L2; func inclusion g -> Function of (Image g),L2 equals :: WAYBEL_1:def 17 id (Image g); coherence id (Image g) is Function of (Image g),L2 proof A1: rng (id (Image g)) = the carrier of (Image g) by RELAT_1:45 .= rng g by YELLOW_0:def_15 ; dom (id (Image g)) = the carrier of (Image g) by RELAT_1:45; hence id (Image g) is Function of (Image g),L2 by A1, RELSET_1:4; ::_thesis: verum end; end; :: deftheorem defines inclusion WAYBEL_1:def_17_:_ for L1, L2 being non empty RelStr for g being Function of L1,L2 holds inclusion g = id (Image g); Lm4: for L1, L2 being non empty RelStr for g being Function of L1,L2 holds inclusion g is monotone proof let L1, L2 be non empty RelStr ; ::_thesis: for g being Function of L1,L2 holds inclusion g is monotone let g be Function of L1,L2; ::_thesis: inclusion g is monotone let s1, s2 be Element of (Image g); :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies (inclusion g) . s1 <= (inclusion g) . s2 ) assume s1 <= s2 ; ::_thesis: (inclusion g) . s1 <= (inclusion g) . s2 then (id (Image g)) . s1 <= s2 by FUNCT_1:18; then (id (Image g)) . s1 <= (id (Image g)) . s2 by FUNCT_1:18; hence (inclusion g) . s1 <= (inclusion g) . s2 by YELLOW_0:59; ::_thesis: verum end; registration let L1, L2 be non empty RelStr ; let g be Function of L1,L2; cluster inclusion g -> V13() monotone ; coherence ( inclusion g is one-to-one & inclusion g is monotone ) by Lm4; end; theorem Th32: :: WAYBEL_1:32 for L being non empty RelStr for f being Function of L,L holds (inclusion f) * (corestr f) = f proof let L be non empty RelStr ; ::_thesis: for f being Function of L,L holds (inclusion f) * (corestr f) = f let f be Function of L,L; ::_thesis: (inclusion f) * (corestr f) = f thus (inclusion f) * (corestr f) = (id the carrier of (Image f)) * f by Th30 .= (id (rng f)) * f by YELLOW_0:def_15 .= f by RELAT_1:54 ; ::_thesis: verum end; theorem Th33: :: WAYBEL_1:33 for L being non empty Poset for f being Function of L,L st f is idempotent holds (corestr f) * (inclusion f) = id (Image f) proof let L be non empty Poset; ::_thesis: for f being Function of L,L st f is idempotent holds (corestr f) * (inclusion f) = id (Image f) let f be Function of L,L; ::_thesis: ( f is idempotent implies (corestr f) * (inclusion f) = id (Image f) ) assume A1: f is idempotent ; ::_thesis: (corestr f) * (inclusion f) = id (Image f) for s being Element of (Image f) holds ((corestr f) * (inclusion f)) . s = s proof let s be Element of (Image f); ::_thesis: ((corestr f) * (inclusion f)) . s = s the carrier of (Image f) = rng (corestr f) by FUNCT_2:def_3; then consider l being set such that A2: l in the carrier of L and A3: (corestr f) . l = s by FUNCT_2:11; reconsider l = l as Element of L by A2; A4: (corestr f) . l = f . l by Th30; thus ((corestr f) * (inclusion f)) . s = (corestr f) . ((inclusion f) . s) by FUNCT_2:15 .= (corestr f) . s by FUNCT_1:18 .= f . (f . l) by A3, A4, Th30 .= s by A1, A3, A4, YELLOW_2:18 ; ::_thesis: verum end; hence (corestr f) * (inclusion f) = id (Image f) by FUNCT_2:124; ::_thesis: verum end; theorem :: WAYBEL_1:34 for L being non empty Poset for f being Function of L,L st f is projection holds ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st ( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) proof let L be non empty Poset; ::_thesis: for f being Function of L,L st f is projection holds ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st ( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) let f be Function of L,L; ::_thesis: ( f is projection implies ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st ( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) ) reconsider T = Image f as non empty Poset ; reconsider q = corestr f as Function of L,T ; reconsider i = inclusion f as Function of T,L ; assume f is projection ; ::_thesis: ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st ( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) then A1: ( f is monotone & f is idempotent ) by Def13; take T ; ::_thesis: ex q being Function of L,T ex i being Function of T,L st ( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) take q ; ::_thesis: ex i being Function of T,L st ( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) take i ; ::_thesis: ( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) thus q is monotone by A1, Th31; ::_thesis: ( q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) thus q is onto ; ::_thesis: ( i is monotone & i is V13() & f = i * q & id T = q * i ) thus ( i is monotone & i is V13() ) ; ::_thesis: ( f = i * q & id T = q * i ) thus f = i * q by Th32; ::_thesis: id T = q * i thus id T = q * i by A1, Th33; ::_thesis: verum end; theorem :: WAYBEL_1:35 for L being non empty Poset for f being Function of L,L st ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st ( q is monotone & i is monotone & f = i * q & id T = q * i ) holds f is projection proof let L be non empty Poset; ::_thesis: for f being Function of L,L st ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st ( q is monotone & i is monotone & f = i * q & id T = q * i ) holds f is projection let f be Function of L,L; ::_thesis: ( ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st ( q is monotone & i is monotone & f = i * q & id T = q * i ) implies f is projection ) given T being non empty Poset, q being Function of L,T, i being Function of T,L such that A1: ( q is monotone & i is monotone ) and A2: f = i * q and A3: id T = q * i ; ::_thesis: f is projection (i * q) * i = i * (id the carrier of T) by A3, RELAT_1:36 .= i by FUNCT_2:17 ; hence f is idempotent by A2, Th21; :: according to WAYBEL_1:def_13 ::_thesis: f is monotone thus f is monotone by A1, A2, YELLOW_2:12; ::_thesis: verum end; theorem Th36: :: WAYBEL_1:36 for L being non empty Poset for f being Function of L,L st f is closure holds [(inclusion f),(corestr f)] is Galois proof let L be non empty Poset; ::_thesis: for f being Function of L,L st f is closure holds [(inclusion f),(corestr f)] is Galois let f be Function of L,L; ::_thesis: ( f is closure implies [(inclusion f),(corestr f)] is Galois ) assume that A1: ( f is idempotent & f is monotone ) and A2: id L <= f ; :: according to WAYBEL_1:def_13,WAYBEL_1:def_14 ::_thesis: [(inclusion f),(corestr f)] is Galois set g = corestr f; set d = inclusion f; (corestr f) * (inclusion f) = id (Image f) by A1, Th33; then A3: (corestr f) * (inclusion f) <= id (Image f) by Lm1; ( corestr f is monotone & id L <= (inclusion f) * (corestr f) ) by A1, A2, Th31, Th32; hence [(inclusion f),(corestr f)] is Galois by A3, Th19; ::_thesis: verum end; theorem :: WAYBEL_1:37 for L being non empty Poset for f being Function of L,L st f is closure holds ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) proof let L be non empty Poset; ::_thesis: for f being Function of L,L st f is closure holds ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) let f be Function of L,L; ::_thesis: ( f is closure implies ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) ) assume A1: f is closure ; ::_thesis: ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) reconsider S = Image f as non empty Poset ; reconsider g = inclusion f as Function of S,L ; reconsider d = corestr f as Function of L,S ; take S ; ::_thesis: ex g being Function of S,L ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) take g ; ::_thesis: ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) take d ; ::_thesis: ( [g,d] is Galois & f = g * d ) thus [g,d] is Galois by A1, Th36; ::_thesis: f = g * d thus f = g * d by Th32; ::_thesis: verum end; theorem Th38: :: WAYBEL_1:38 for L being non empty Poset for f being Function of L,L st f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) holds f is closure proof let L be non empty Poset; ::_thesis: for f being Function of L,L st f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) holds f is closure let f be Function of L,L; ::_thesis: ( f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st ( [g,d] is Galois & f = g * d ) implies f is closure ) assume A1: f is monotone ; ::_thesis: ( for S being non empty Poset for g being Function of S,L for d being Function of L,S holds ( not [g,d] is Galois or not f = g * d ) or f is closure ) given S being non empty Poset, g being Function of S,L, d being Function of L,S such that A2: [g,d] is Galois and A3: f = g * d ; ::_thesis: f is closure A4: ( d is monotone & g is monotone ) by A2, Th8; ( d * g <= id S & id L <= g * d ) by A2, Th18; then g = (g * d) * g by A4, Th20; hence ( f is idempotent & f is monotone ) by A1, A3, Th21; :: according to WAYBEL_1:def_13,WAYBEL_1:def_14 ::_thesis: id L <= f thus id L <= f by A2, A3, Th18; ::_thesis: verum end; theorem Th39: :: WAYBEL_1:39 for L being non empty Poset for f being Function of L,L st f is kernel holds [(corestr f),(inclusion f)] is Galois proof let L be non empty Poset; ::_thesis: for f being Function of L,L st f is kernel holds [(corestr f),(inclusion f)] is Galois let f be Function of L,L; ::_thesis: ( f is kernel implies [(corestr f),(inclusion f)] is Galois ) assume that A1: ( f is idempotent & f is monotone ) and A2: f <= id L ; :: according to WAYBEL_1:def_13,WAYBEL_1:def_15 ::_thesis: [(corestr f),(inclusion f)] is Galois set g = corestr f; set d = inclusion f; (corestr f) * (inclusion f) = id (Image f) by A1, Th33; then A3: id (Image f) <= (corestr f) * (inclusion f) by Lm1; ( corestr f is monotone & (inclusion f) * (corestr f) <= id L ) by A1, A2, Th31, Th32; hence [(corestr f),(inclusion f)] is Galois by A3, Th19; ::_thesis: verum end; theorem :: WAYBEL_1:40 for L being non empty Poset for f being Function of L,L st f is kernel holds ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) proof let L be non empty Poset; ::_thesis: for f being Function of L,L st f is kernel holds ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) let f be Function of L,L; ::_thesis: ( f is kernel implies ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) ) assume A1: f is kernel ; ::_thesis: ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) reconsider T = Image f as non empty Poset ; reconsider g = corestr f as Function of L,T ; reconsider d = inclusion f as Function of T,L ; take T ; ::_thesis: ex g being Function of L,T ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) take g ; ::_thesis: ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) take d ; ::_thesis: ( [g,d] is Galois & f = d * g ) thus [g,d] is Galois by A1, Th39; ::_thesis: f = d * g thus f = d * g by Th32; ::_thesis: verum end; theorem :: WAYBEL_1:41 for L being non empty Poset for f being Function of L,L st f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) holds f is kernel proof let L be non empty Poset; ::_thesis: for f being Function of L,L st f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) holds f is kernel let f be Function of L,L; ::_thesis: ( f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st ( [g,d] is Galois & f = d * g ) implies f is kernel ) assume A1: f is monotone ; ::_thesis: ( for T being non empty Poset for g being Function of L,T for d being Function of T,L holds ( not [g,d] is Galois or not f = d * g ) or f is kernel ) given T being non empty Poset, g being Function of L,T, d being Function of T,L such that A2: [g,d] is Galois and A3: f = d * g ; ::_thesis: f is kernel A4: ( d is monotone & g is monotone ) by A2, Th8; ( d * g <= id L & id T <= g * d ) by A2, Th18; then d = (d * g) * d by A4, Th20; hence ( f is idempotent & f is monotone ) by A1, A3, Th21; :: according to WAYBEL_1:def_13,WAYBEL_1:def_15 ::_thesis: f <= id L thus f <= id L by A2, A3, Th18; ::_thesis: verum end; theorem Th42: :: WAYBEL_1:42 for L being non empty Poset for p being Function of L,L st p is projection holds rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } let p be Function of L,L; ::_thesis: ( p is projection implies rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } ) assume that A1: p is idempotent and p is monotone ; :: according to WAYBEL_1:def_13 ::_thesis: rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } set Lk = { k where k is Element of L : p . k <= k } ; set Lc = { c where c is Element of L : c <= p . c } ; thus rng p c= { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } :: according to XBOOLE_0:def_10 ::_thesis: { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } c= rng p proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } ) assume A2: x in rng p ; ::_thesis: x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } then reconsider x9 = x as Element of L ; A3: ex l being set st ( l in dom p & p . l = x ) by A2, FUNCT_1:def_3; then p . x9 <= x9 by A1, YELLOW_2:18; then A4: x in { k where k is Element of L : p . k <= k } ; x9 <= p . x9 by A1, A3, YELLOW_2:18; then x in { c where c is Element of L : c <= p . c } ; hence x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } by A4, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } or x in rng p ) assume A5: x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } ; ::_thesis: x in rng p then x in { c where c is Element of L : c <= p . c } by XBOOLE_0:def_4; then A6: ex lc being Element of L st ( x = lc & lc <= p . lc ) ; x in { k where k is Element of L : p . k <= k } by A5, XBOOLE_0:def_4; then ex lk being Element of L st ( x = lk & p . lk <= lk ) ; then ( dom p = the carrier of L & x = p . x ) by A6, FUNCT_2:def_1, ORDERS_2:2; hence x in rng p by A6, FUNCT_1:def_3; ::_thesis: verum end; theorem Th43: :: WAYBEL_1:43 for L being non empty Poset for p being Function of L,L st p is projection holds ( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L ) proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds ( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L ) let p be Function of L,L; ::_thesis: ( p is projection implies ( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L ) ) assume A1: p is projection ; ::_thesis: ( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L ) defpred S1[ Element of L] means p . $1 <= $1; defpred S2[ Element of L] means $1 <= p . $1; set Lc = { c where c is Element of L : S2[c] } ; set Lk = { k where k is Element of L : S1[k] } ; A2: rng p = { c where c is Element of L : S2[c] } /\ { k where k is Element of L : S1[k] } by A1, Th42; { c where c is Element of L : S2[c] } is Subset of L from DOMAIN_1:sch_7(); hence { c where c is Element of L : S2[c] } is non empty Subset of L by A2; ::_thesis: { k where k is Element of L : p . k <= k } is non empty Subset of L { k where k is Element of L : S1[k] } is Subset of L from DOMAIN_1:sch_7(); hence { k where k is Element of L : p . k <= k } is non empty Subset of L by A2; ::_thesis: verum end; theorem Th44: :: WAYBEL_1:44 for L being non empty Poset for p being Function of L,L st p is projection holds ( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p ) proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds ( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p ) let p be Function of L,L; ::_thesis: ( p is projection implies ( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p ) ) assume A1: p is projection ; ::_thesis: ( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p ) set Lk = { k where k is Element of L : p . k <= k } ; set Lc = { c where c is Element of L : c <= p . c } ; A2: rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } by A1, Th42; A3: dom p = the carrier of L by FUNCT_2:def_1; thus rng (p | { c where c is Element of L : c <= p . c } ) = rng p ::_thesis: rng (p | { k where k is Element of L : p . k <= k } ) = rng p proof thus rng (p | { c where c is Element of L : c <= p . c } ) c= rng p by RELAT_1:70; :: according to XBOOLE_0:def_10 ::_thesis: rng p c= rng (p | { c where c is Element of L : c <= p . c } ) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in rng (p | { c where c is Element of L : c <= p . c } ) ) assume A4: y in rng p ; ::_thesis: y in rng (p | { c where c is Element of L : c <= p . c } ) then A5: y in { c where c is Element of L : c <= p . c } by A2, XBOOLE_0:def_4; then A6: ex lc being Element of L st ( y = lc & lc <= p . lc ) ; y in { k where k is Element of L : p . k <= k } by A2, A4, XBOOLE_0:def_4; then ex lk being Element of L st ( y = lk & p . lk <= lk ) ; then y = p . y by A6, ORDERS_2:2; hence y in rng (p | { c where c is Element of L : c <= p . c } ) by A3, A5, A6, FUNCT_1:50; ::_thesis: verum end; thus rng (p | { k where k is Element of L : p . k <= k } ) c= rng p by RELAT_1:70; :: according to XBOOLE_0:def_10 ::_thesis: rng p c= rng (p | { k where k is Element of L : p . k <= k } ) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in rng (p | { k where k is Element of L : p . k <= k } ) ) assume A7: y in rng p ; ::_thesis: y in rng (p | { k where k is Element of L : p . k <= k } ) then y in { c where c is Element of L : c <= p . c } by A2, XBOOLE_0:def_4; then A8: ex lc being Element of L st ( y = lc & lc <= p . lc ) ; A9: y in { k where k is Element of L : p . k <= k } by A2, A7, XBOOLE_0:def_4; then ex lk being Element of L st ( y = lk & p . lk <= lk ) ; then y = p . y by A8, ORDERS_2:2; hence y in rng (p | { k where k is Element of L : p . k <= k } ) by A3, A9, A8, FUNCT_1:50; ::_thesis: verum end; theorem Th45: :: WAYBEL_1:45 for L being non empty Poset for p being Function of L,L st p is projection holds for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds p | Lc is Function of (subrelstr Lc),(subrelstr Lc) proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds p | Lc is Function of (subrelstr Lc),(subrelstr Lc) let p be Function of L,L; ::_thesis: ( p is projection implies for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds p | Lc is Function of (subrelstr Lc),(subrelstr Lc) ) assume A1: p is projection ; ::_thesis: for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds p | Lc is Function of (subrelstr Lc),(subrelstr Lc) let Lc, Lk be non empty Subset of L; ::_thesis: ( Lc = { c where c is Element of L : c <= p . c } implies p | Lc is Function of (subrelstr Lc),(subrelstr Lc) ) assume A2: Lc = { c where c is Element of L : c <= p . c } ; ::_thesis: p | Lc is Function of (subrelstr Lc),(subrelstr Lc) set Lk = { k where k is Element of L : p . k <= k } ; rng p = Lc /\ { k where k is Element of L : p . k <= k } by A1, A2, Th42; then rng (p | Lc) = Lc /\ { k where k is Element of L : p . k <= k } by A1, A2, Th44; then A3: rng (p | Lc) c= Lc by XBOOLE_1:17; ( Lc = the carrier of (subrelstr Lc) & p | Lc is Function of Lc, the carrier of L ) by FUNCT_2:32, YELLOW_0:def_15; hence p | Lc is Function of (subrelstr Lc),(subrelstr Lc) by A3, FUNCT_2:6; ::_thesis: verum end; theorem :: WAYBEL_1:46 for L being non empty Poset for p being Function of L,L st p is projection holds for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds p | Lk is Function of (subrelstr Lk),(subrelstr Lk) proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds p | Lk is Function of (subrelstr Lk),(subrelstr Lk) let p be Function of L,L; ::_thesis: ( p is projection implies for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds p | Lk is Function of (subrelstr Lk),(subrelstr Lk) ) assume A1: p is projection ; ::_thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds p | Lk is Function of (subrelstr Lk),(subrelstr Lk) set Lc = { c where c is Element of L : c <= p . c } ; let Lk be non empty Subset of L; ::_thesis: ( Lk = { k where k is Element of L : p . k <= k } implies p | Lk is Function of (subrelstr Lk),(subrelstr Lk) ) assume A2: Lk = { k where k is Element of L : p . k <= k } ; ::_thesis: p | Lk is Function of (subrelstr Lk),(subrelstr Lk) rng p = { c where c is Element of L : c <= p . c } /\ Lk by A1, A2, Th42; then rng (p | Lk) = { c where c is Element of L : c <= p . c } /\ Lk by A1, A2, Th44; then A3: rng (p | Lk) c= Lk by XBOOLE_1:17; ( Lk = the carrier of (subrelstr Lk) & p | Lk is Function of Lk, the carrier of L ) by FUNCT_2:32, YELLOW_0:def_15; hence p | Lk is Function of (subrelstr Lk),(subrelstr Lk) by A3, FUNCT_2:6; ::_thesis: verum end; theorem Th47: :: WAYBEL_1:47 for L being non empty Poset for p being Function of L,L st p is projection holds for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds pc is closure proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds pc is closure let p be Function of L,L; ::_thesis: ( p is projection implies for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds pc is closure ) assume that A1: p is idempotent and A2: p is monotone ; :: according to WAYBEL_1:def_13 ::_thesis: for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds pc is closure let Lc be non empty Subset of L; ::_thesis: ( Lc = { c where c is Element of L : c <= p . c } implies for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds pc is closure ) assume A3: Lc = { c where c is Element of L : c <= p . c } ; ::_thesis: for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds pc is closure let pc be Function of (subrelstr Lc),(subrelstr Lc); ::_thesis: ( pc = p | Lc implies pc is closure ) assume A4: pc = p | Lc ; ::_thesis: pc is closure A5: dom pc = the carrier of (subrelstr Lc) by FUNCT_2:def_1; hereby :: according to QUANTAL1:def_9,WAYBEL_1:def_13,WAYBEL_1:def_14 ::_thesis: id (subrelstr Lc) <= pc now__::_thesis:_for_x_being_Element_of_(subrelstr_Lc)_holds_(pc_*_pc)_._x_=_pc_._x let x be Element of (subrelstr Lc); ::_thesis: (pc * pc) . x = pc . x A6: x is Element of L by YELLOW_0:58; A7: pc . x = p . x by A4, A5, FUNCT_1:47; then p . (p . x) = pc . (pc . x) by A4, A5, FUNCT_1:47 .= (pc * pc) . x by A5, FUNCT_1:13 ; hence (pc * pc) . x = pc . x by A1, A7, A6, YELLOW_2:18; ::_thesis: verum end; hence pc * pc = pc by FUNCT_2:63; ::_thesis: pc is monotone thus pc is monotone ::_thesis: verum proof let x1, x2 be Element of (subrelstr Lc); :: according to WAYBEL_1:def_2 ::_thesis: ( x1 <= x2 implies pc . x1 <= pc . x2 ) reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58; assume x1 <= x2 ; ::_thesis: pc . x1 <= pc . x2 then x19 <= x29 by YELLOW_0:59; then A8: p . x19 <= p . x29 by A2, Def2; ( pc . x1 = p . x19 & pc . x2 = p . x29 ) by A4, A5, FUNCT_1:47; hence pc . x1 <= pc . x2 by A8, YELLOW_0:60; ::_thesis: verum end; end; now__::_thesis:_for_x_being_Element_of_(subrelstr_Lc)_holds_(id_(subrelstr_Lc))_._x_<=_pc_._x let x be Element of (subrelstr Lc); ::_thesis: (id (subrelstr Lc)) . x <= pc . x reconsider x9 = x as Element of L by YELLOW_0:58; x in the carrier of (subrelstr Lc) ; then x in Lc by YELLOW_0:def_15; then A9: ex c being Element of L st ( x = c & c <= p . c ) by A3; pc . x = p . x9 by A4, A5, FUNCT_1:47; then x <= pc . x by A9, YELLOW_0:60; hence (id (subrelstr Lc)) . x <= pc . x by FUNCT_1:18; ::_thesis: verum end; hence id (subrelstr Lc) <= pc by YELLOW_2:9; ::_thesis: verum end; theorem :: WAYBEL_1:48 for L being non empty Poset for p being Function of L,L st p is projection holds for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds pk is kernel proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds pk is kernel let p be Function of L,L; ::_thesis: ( p is projection implies for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds pk is kernel ) assume that A1: p is idempotent and A2: p is monotone ; :: according to WAYBEL_1:def_13 ::_thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds pk is kernel let Lk be non empty Subset of L; ::_thesis: ( Lk = { k where k is Element of L : p . k <= k } implies for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds pk is kernel ) assume A3: Lk = { k where k is Element of L : p . k <= k } ; ::_thesis: for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds pk is kernel let pk be Function of (subrelstr Lk),(subrelstr Lk); ::_thesis: ( pk = p | Lk implies pk is kernel ) assume A4: pk = p | Lk ; ::_thesis: pk is kernel A5: dom pk = the carrier of (subrelstr Lk) by FUNCT_2:def_1; hereby :: according to QUANTAL1:def_9,WAYBEL_1:def_13,WAYBEL_1:def_15 ::_thesis: pk <= id (subrelstr Lk) now__::_thesis:_for_x_being_Element_of_(subrelstr_Lk)_holds_(pk_*_pk)_._x_=_pk_._x let x be Element of (subrelstr Lk); ::_thesis: (pk * pk) . x = pk . x A6: x is Element of L by YELLOW_0:58; A7: pk . x = p . x by A4, A5, FUNCT_1:47; then p . (p . x) = pk . (pk . x) by A4, A5, FUNCT_1:47 .= (pk * pk) . x by A5, FUNCT_1:13 ; hence (pk * pk) . x = pk . x by A1, A7, A6, YELLOW_2:18; ::_thesis: verum end; hence pk * pk = pk by FUNCT_2:63; ::_thesis: pk is monotone thus pk is monotone ::_thesis: verum proof let x1, x2 be Element of (subrelstr Lk); :: according to WAYBEL_1:def_2 ::_thesis: ( x1 <= x2 implies pk . x1 <= pk . x2 ) reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58; assume x1 <= x2 ; ::_thesis: pk . x1 <= pk . x2 then x19 <= x29 by YELLOW_0:59; then A8: p . x19 <= p . x29 by A2, Def2; ( pk . x1 = p . x19 & pk . x2 = p . x29 ) by A4, A5, FUNCT_1:47; hence pk . x1 <= pk . x2 by A8, YELLOW_0:60; ::_thesis: verum end; end; now__::_thesis:_for_x_being_Element_of_(subrelstr_Lk)_holds_pk_._x_<=_(id_(subrelstr_Lk))_._x let x be Element of (subrelstr Lk); ::_thesis: pk . x <= (id (subrelstr Lk)) . x reconsider x9 = x as Element of L by YELLOW_0:58; x in the carrier of (subrelstr Lk) ; then x in Lk by YELLOW_0:def_15; then A9: ex c being Element of L st ( x = c & p . c <= c ) by A3; pk . x = p . x9 by A4, A5, FUNCT_1:47; then pk . x <= x by A9, YELLOW_0:60; hence pk . x <= (id (subrelstr Lk)) . x by FUNCT_1:18; ::_thesis: verum end; hence pk <= id (subrelstr Lk) by YELLOW_2:9; ::_thesis: verum end; theorem Th49: :: WAYBEL_1:49 for L being non empty Poset for p being Function of L,L st p is monotone holds for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds subrelstr Lc is sups-inheriting proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is monotone holds for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds subrelstr Lc is sups-inheriting let p be Function of L,L; ::_thesis: ( p is monotone implies for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds subrelstr Lc is sups-inheriting ) assume A1: p is monotone ; ::_thesis: for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds subrelstr Lc is sups-inheriting let Lc be Subset of L; ::_thesis: ( Lc = { c where c is Element of L : c <= p . c } implies subrelstr Lc is sups-inheriting ) assume A2: Lc = { c where c is Element of L : c <= p . c } ; ::_thesis: subrelstr Lc is sups-inheriting let X be Subset of (subrelstr Lc); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr Lc) ) assume A3: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr Lc) p . ("\/" (X,L)) is_>=_than X proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= p . ("\/" (X,L)) ) assume A4: x in X ; ::_thesis: x <= p . ("\/" (X,L)) then x in the carrier of (subrelstr Lc) ; then x in Lc by YELLOW_0:def_15; then A5: ex l being Element of L st ( x = l & l <= p . l ) by A2; "\/" (X,L) is_>=_than X by A3, YELLOW_0:30; then x <= "\/" (X,L) by A4, LATTICE3:def_9; then p . x <= p . ("\/" (X,L)) by A1, Def2; hence x <= p . ("\/" (X,L)) by A5, ORDERS_2:3; ::_thesis: verum end; then "\/" (X,L) <= p . ("\/" (X,L)) by A3, YELLOW_0:30; then "\/" (X,L) in Lc by A2; hence "\/" (X,L) in the carrier of (subrelstr Lc) by YELLOW_0:def_15; ::_thesis: verum end; theorem Th50: :: WAYBEL_1:50 for L being non empty Poset for p being Function of L,L st p is monotone holds for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds subrelstr Lk is infs-inheriting proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is monotone holds for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds subrelstr Lk is infs-inheriting let p be Function of L,L; ::_thesis: ( p is monotone implies for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds subrelstr Lk is infs-inheriting ) assume A1: p is monotone ; ::_thesis: for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds subrelstr Lk is infs-inheriting let Lk be Subset of L; ::_thesis: ( Lk = { k where k is Element of L : p . k <= k } implies subrelstr Lk is infs-inheriting ) assume A2: Lk = { k where k is Element of L : p . k <= k } ; ::_thesis: subrelstr Lk is infs-inheriting let X be Subset of (subrelstr Lk); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr Lk) ) assume A3: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (subrelstr Lk) p . ("/\" (X,L)) is_<=_than X proof let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X or p . ("/\" (X,L)) <= x ) assume A4: x in X ; ::_thesis: p . ("/\" (X,L)) <= x then x in the carrier of (subrelstr Lk) ; then x in Lk by YELLOW_0:def_15; then A5: ex l being Element of L st ( x = l & l >= p . l ) by A2; "/\" (X,L) is_<=_than X by A3, YELLOW_0:31; then x >= "/\" (X,L) by A4, LATTICE3:def_8; then p . x >= p . ("/\" (X,L)) by A1, Def2; hence p . ("/\" (X,L)) <= x by A5, ORDERS_2:3; ::_thesis: verum end; then "/\" (X,L) >= p . ("/\" (X,L)) by A3, YELLOW_0:31; then "/\" (X,L) in Lk by A2; hence "/\" (X,L) in the carrier of (subrelstr Lk) by YELLOW_0:def_15; ::_thesis: verum end; theorem :: WAYBEL_1:51 for L being non empty Poset for p being Function of L,L st p is projection holds for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds ( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) ) proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds ( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) ) let p be Function of L,L; ::_thesis: ( p is projection implies for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds ( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) ) ) assume A1: p is projection ; ::_thesis: for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds ( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) ) then reconsider Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by Th43; let Lc be non empty Subset of L; ::_thesis: ( Lc = { c where c is Element of L : c <= p . c } implies ( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) ) ) assume A2: Lc = { c where c is Element of L : c <= p . c } ; ::_thesis: ( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) ) A3: p is monotone by A1, Def13; then A4: subrelstr Lk is infs-inheriting by Th50; A5: Lc = the carrier of (subrelstr Lc) by YELLOW_0:def_15; A6: the carrier of (Image p) = rng p by YELLOW_0:def_15 .= Lc /\ Lk by A1, A2, Th42 ; then A7: the carrier of (Image p) c= Lk by XBOOLE_1:17; A8: Lk = the carrier of (subrelstr Lk) by YELLOW_0:def_15; A9: the carrier of (Image p) c= Lc by A6, XBOOLE_1:17; hereby ::_thesis: ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) assume A10: p is infs-preserving ; ::_thesis: ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) thus A11: subrelstr Lc is infs-inheriting ::_thesis: Image p is infs-inheriting proof let X be Subset of (subrelstr Lc); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr Lc) ) the carrier of (subrelstr Lc) is Subset of L by YELLOW_0:def_15; then reconsider X9 = X as Subset of L by XBOOLE_1:1; assume A12: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (subrelstr Lc) A13: inf X9 is_<=_than p .: X9 proof let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in p .: X9 or inf X9 <= y ) assume y in p .: X9 ; ::_thesis: inf X9 <= y then consider x being Element of L such that A14: x in X9 and A15: y = p . x by FUNCT_2:65; reconsider x = x as Element of L ; x in Lc by A5, A14; then A16: ex x9 being Element of L st ( x9 = x & x9 <= p . x9 ) by A2; inf X9 is_<=_than X9 by A12, YELLOW_0:31; then inf X9 <= x by A14, LATTICE3:def_8; hence inf X9 <= y by A15, A16, ORDERS_2:3; ::_thesis: verum end; p preserves_inf_of X9 by A10, WAYBEL_0:def_32; then ( ex_inf_of p .: X,L & inf (p .: X9) = p . (inf X9) ) by A12, WAYBEL_0:def_30; then inf X9 <= p . (inf X9) by A13, YELLOW_0:31; hence "/\" (X,L) in the carrier of (subrelstr Lc) by A2, A5; ::_thesis: verum end; thus Image p is infs-inheriting ::_thesis: verum proof let X be Subset of (Image p); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (Image p) ) assume A17: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (Image p) X c= Lc by A9, XBOOLE_1:1; then A18: "/\" (X,L) in the carrier of (subrelstr Lc) by A5, A11, A17, YELLOW_0:def_18; ( subrelstr Lk is infs-inheriting & X c= the carrier of (subrelstr Lk) ) by A3, A7, A8, Th50, XBOOLE_1:1; then "/\" (X,L) in the carrier of (subrelstr Lk) by A17, YELLOW_0:def_18; hence "/\" (X,L) in the carrier of (Image p) by A6, A5, A8, A18, XBOOLE_0:def_4; ::_thesis: verum end; end; assume A19: p is filtered-infs-preserving ; ::_thesis: ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) thus A20: subrelstr Lc is filtered-infs-inheriting ::_thesis: Image p is filtered-infs-inheriting proof let X be filtered Subset of (subrelstr Lc); :: according to WAYBEL_0:def_3 ::_thesis: ( X = {} or not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr Lc) ) assume X <> {} ; ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr Lc) ) then reconsider X9 = X as non empty filtered Subset of L by YELLOW_2:7; assume A21: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (subrelstr Lc) A22: inf X9 is_<=_than p .: X9 proof let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in p .: X9 or inf X9 <= y ) assume y in p .: X9 ; ::_thesis: inf X9 <= y then consider x being Element of L such that A23: x in X9 and A24: y = p . x by FUNCT_2:65; reconsider x = x as Element of L ; x in Lc by A5, A23; then A25: ex x9 being Element of L st ( x9 = x & x9 <= p . x9 ) by A2; inf X9 is_<=_than X9 by A21, YELLOW_0:31; then inf X9 <= x by A23, LATTICE3:def_8; hence inf X9 <= y by A24, A25, ORDERS_2:3; ::_thesis: verum end; p preserves_inf_of X9 by A19, WAYBEL_0:def_36; then ( ex_inf_of p .: X,L & inf (p .: X9) = p . (inf X9) ) by A21, WAYBEL_0:def_30; then inf X9 <= p . (inf X9) by A22, YELLOW_0:31; hence "/\" (X,L) in the carrier of (subrelstr Lc) by A2, A5; ::_thesis: verum end; let X be filtered Subset of (Image p); :: according to WAYBEL_0:def_3 ::_thesis: ( X = {} or not ex_inf_of X,L or "/\" (X,L) in the carrier of (Image p) ) assume that A26: X <> {} and A27: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (Image p) the carrier of (Image p) c= the carrier of (subrelstr Lc) by A9, YELLOW_0:def_15; then X is filtered Subset of (subrelstr Lc) by YELLOW_2:8; then A28: "/\" (X,L) in the carrier of (subrelstr Lc) by A20, A26, A27, WAYBEL_0:def_3; X c= the carrier of (subrelstr Lk) by A7, A8, XBOOLE_1:1; then "/\" (X,L) in the carrier of (subrelstr Lk) by A27, A4, YELLOW_0:def_18; hence "/\" (X,L) in the carrier of (Image p) by A6, A5, A8, A28, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: WAYBEL_1:52 for L being non empty Poset for p being Function of L,L st p is projection holds for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds ( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) ) proof let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds ( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) ) let p be Function of L,L; ::_thesis: ( p is projection implies for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds ( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) ) ) assume A1: p is projection ; ::_thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds ( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) ) then reconsider Lc = { c where c is Element of L : c <= p . c } as non empty Subset of L by Th43; let Lk be non empty Subset of L; ::_thesis: ( Lk = { k where k is Element of L : p . k <= k } implies ( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) ) ) assume A2: Lk = { k where k is Element of L : p . k <= k } ; ::_thesis: ( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) ) A3: p is monotone by A1, Def13; then A4: subrelstr Lc is sups-inheriting by Th49; A5: Lc = the carrier of (subrelstr Lc) by YELLOW_0:def_15; A6: the carrier of (Image p) = rng p by YELLOW_0:def_15 .= Lc /\ Lk by A1, A2, Th42 ; then A7: the carrier of (Image p) c= Lk by XBOOLE_1:17; A8: Lk = the carrier of (subrelstr Lk) by YELLOW_0:def_15; A9: the carrier of (Image p) c= Lc by A6, XBOOLE_1:17; hereby ::_thesis: ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) assume A10: p is sups-preserving ; ::_thesis: ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) thus A11: subrelstr Lk is sups-inheriting ::_thesis: Image p is sups-inheriting proof let X be Subset of (subrelstr Lk); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr Lk) ) the carrier of (subrelstr Lk) is Subset of L by YELLOW_0:def_15; then reconsider X9 = X as Subset of L by XBOOLE_1:1; assume A12: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr Lk) A13: sup X9 is_>=_than p .: X9 proof let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in p .: X9 or y <= sup X9 ) assume y in p .: X9 ; ::_thesis: y <= sup X9 then consider x being Element of L such that A14: x in X9 and A15: y = p . x by FUNCT_2:65; reconsider x = x as Element of L ; x in Lk by A8, A14; then A16: ex x9 being Element of L st ( x9 = x & x9 >= p . x9 ) by A2; sup X9 is_>=_than X9 by A12, YELLOW_0:30; then sup X9 >= x by A14, LATTICE3:def_9; hence y <= sup X9 by A15, A16, ORDERS_2:3; ::_thesis: verum end; p preserves_sup_of X9 by A10, WAYBEL_0:def_33; then ( ex_sup_of p .: X,L & sup (p .: X9) = p . (sup X9) ) by A12, WAYBEL_0:def_31; then sup X9 >= p . (sup X9) by A13, YELLOW_0:30; hence "\/" (X,L) in the carrier of (subrelstr Lk) by A2, A8; ::_thesis: verum end; thus Image p is sups-inheriting ::_thesis: verum proof let X be Subset of (Image p); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image p) ) assume A17: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (Image p) X c= Lk by A7, XBOOLE_1:1; then A18: "\/" (X,L) in the carrier of (subrelstr Lk) by A8, A11, A17, YELLOW_0:def_19; ( subrelstr Lc is sups-inheriting & X c= the carrier of (subrelstr Lc) ) by A3, A9, A5, Th49, XBOOLE_1:1; then "\/" (X,L) in the carrier of (subrelstr Lc) by A17, YELLOW_0:def_19; hence "\/" (X,L) in the carrier of (Image p) by A6, A5, A8, A18, XBOOLE_0:def_4; ::_thesis: verum end; end; assume A19: p is directed-sups-preserving ; ::_thesis: ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) thus A20: subrelstr Lk is directed-sups-inheriting ::_thesis: Image p is directed-sups-inheriting proof let X be directed Subset of (subrelstr Lk); :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr Lk) ) assume X <> {} ; ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr Lk) ) then reconsider X9 = X as non empty directed Subset of L by YELLOW_2:7; assume A21: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr Lk) A22: sup X9 is_>=_than p .: X9 proof let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in p .: X9 or y <= sup X9 ) assume y in p .: X9 ; ::_thesis: y <= sup X9 then consider x being Element of L such that A23: x in X9 and A24: y = p . x by FUNCT_2:65; reconsider x = x as Element of L ; x in Lk by A8, A23; then A25: ex x9 being Element of L st ( x9 = x & x9 >= p . x9 ) by A2; sup X9 is_>=_than X9 by A21, YELLOW_0:30; then sup X9 >= x by A23, LATTICE3:def_9; hence y <= sup X9 by A24, A25, ORDERS_2:3; ::_thesis: verum end; p preserves_sup_of X9 by A19, WAYBEL_0:def_37; then ( ex_sup_of p .: X,L & sup (p .: X9) = p . (sup X9) ) by A21, WAYBEL_0:def_31; then sup X9 >= p . (sup X9) by A22, YELLOW_0:30; hence "\/" (X,L) in the carrier of (subrelstr Lk) by A2, A8; ::_thesis: verum end; let X be directed Subset of (Image p); :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image p) ) assume that A26: X <> {} and A27: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (Image p) the carrier of (Image p) c= the carrier of (subrelstr Lk) by A7, YELLOW_0:def_15; then X is directed Subset of (subrelstr Lk) by YELLOW_2:8; then A28: "\/" (X,L) in the carrier of (subrelstr Lk) by A20, A26, A27, WAYBEL_0:def_4; X c= the carrier of (subrelstr Lc) by A9, A5, XBOOLE_1:1; then "\/" (X,L) in the carrier of (subrelstr Lc) by A27, A4, YELLOW_0:def_19; hence "\/" (X,L) in the carrier of (Image p) by A6, A5, A8, A28, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th53: :: WAYBEL_1:53 for L being non empty Poset for p being Function of L,L holds ( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) ) proof let L be non empty Poset; ::_thesis: for p being Function of L,L holds ( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) ) let p be Function of L,L; ::_thesis: ( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) ) hereby ::_thesis: ( p is kernel implies Image p is sups-inheriting ) assume A1: p is closure ; ::_thesis: Image p is infs-inheriting thus Image p is infs-inheriting ::_thesis: verum proof let X be Subset of (Image p); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (Image p) ) A2: the carrier of (Image p) = rng p by YELLOW_0:def_15; then reconsider X9 = X as Subset of L by XBOOLE_1:1; assume ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (Image p) then p . ("/\" (X9,L)) = "/\" (X9,L) by A1, A2, Th28; hence "/\" (X,L) in the carrier of (Image p) by A2, FUNCT_2:4; ::_thesis: verum end; end; assume A3: p is kernel ; ::_thesis: Image p is sups-inheriting let X be Subset of (Image p); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image p) ) A4: the carrier of (Image p) = rng p by YELLOW_0:def_15; then reconsider X9 = X as Subset of L by XBOOLE_1:1; assume ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (Image p) then p . ("\/" (X9,L)) = "\/" (X9,L) by A3, A4, Th29; hence "\/" (X,L) in the carrier of (Image p) by A4, FUNCT_2:4; ::_thesis: verum end; theorem :: WAYBEL_1:54 for L being non empty complete Poset for p being Function of L,L st p is projection holds Image p is complete proof let L be non empty complete Poset; ::_thesis: for p being Function of L,L st p is projection holds Image p is complete let p be Function of L,L; ::_thesis: ( p is projection implies Image p is complete ) A1: the carrier of (Image p) = rng p by YELLOW_0:def_15; assume A2: p is projection ; ::_thesis: Image p is complete then reconsider Lc = { c where c is Element of L : c <= p . c } , Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by Th43; A3: ( the carrier of (subrelstr Lc) = Lc & rng p = Lc /\ Lk ) by A2, Th42, YELLOW_0:def_15; p is monotone by A2, Def13; then subrelstr Lc is sups-inheriting by Th49; then A4: subrelstr Lc is complete LATTICE by YELLOW_2:31; reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by A2, Th45; A5: Image pc is infs-inheriting by A2, Th47, Th53; A6: the carrier of (Image pc) = rng pc by YELLOW_0:def_15 .= the carrier of (Image p) by A2, A1, Th44 ; then the InternalRel of (Image pc) = the InternalRel of (subrelstr Lc) |_2 the carrier of (Image p) by YELLOW_0:def_14 .= ( the InternalRel of L |_2 the carrier of (subrelstr Lc)) |_2 the carrier of (Image p) by YELLOW_0:def_14 .= the InternalRel of L |_2 the carrier of (Image p) by A1, A3, WELLORD1:22, XBOOLE_1:17 .= the InternalRel of (Image p) by YELLOW_0:def_14 ; hence Image p is complete by A4, A5, A6, YELLOW_2:30; ::_thesis: verum end; theorem :: WAYBEL_1:55 for L being non empty Poset for c being Function of L,L st c is closure holds ( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) ) proof let L be non empty Poset; ::_thesis: for c being Function of L,L st c is closure holds ( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) ) let c be Function of L,L; ::_thesis: ( c is closure implies ( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) ) ) A1: corestr c = c by Th30; assume A2: c is closure ; ::_thesis: ( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) ) then A3: c is idempotent by Def13; [(inclusion c),(corestr c)] is Galois by A2, Th36; then A4: corestr c is lower_adjoint by Def12; hence corestr c is sups-preserving ; ::_thesis: for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) let X be Subset of L; ::_thesis: ( X c= the carrier of (Image c) & ex_sup_of X,L implies ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) assume that A5: X c= the carrier of (Image c) and A6: ex_sup_of X,L ; ::_thesis: ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) X c= rng c by A5, YELLOW_0:def_15; then A7: c .: X = X by A3, YELLOW_2:20; corestr c preserves_sup_of X by A4, WAYBEL_0:def_33; hence ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) by A6, A1, A7, WAYBEL_0:def_31; ::_thesis: verum end; theorem :: WAYBEL_1:56 for L being non empty Poset for k being Function of L,L st k is kernel holds ( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) ) proof let L be non empty Poset; ::_thesis: for k being Function of L,L st k is kernel holds ( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) ) let k be Function of L,L; ::_thesis: ( k is kernel implies ( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) ) ) A1: corestr k = k by Th30; assume A2: k is kernel ; ::_thesis: ( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) ) then A3: k is idempotent by Def13; [(corestr k),(inclusion k)] is Galois by A2, Th39; then A4: corestr k is upper_adjoint by Def11; hence corestr k is infs-preserving ; ::_thesis: for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) let X be Subset of L; ::_thesis: ( X c= the carrier of (Image k) & ex_inf_of X,L implies ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) assume that A5: X c= the carrier of (Image k) and A6: ex_inf_of X,L ; ::_thesis: ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) X c= rng k by A5, YELLOW_0:def_15; then A7: k .: X = X by A3, YELLOW_2:20; corestr k preserves_inf_of X by A4, WAYBEL_0:def_32; hence ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) by A6, A1, A7, WAYBEL_0:def_30; ::_thesis: verum end; begin theorem Th57: :: WAYBEL_1:57 for L being non empty complete Poset holds ( [(IdsMap L),(SupMap L)] is Galois & SupMap L is sups-preserving ) proof let L be non empty complete Poset; ::_thesis: ( [(IdsMap L),(SupMap L)] is Galois & SupMap L is sups-preserving ) set g = IdsMap L; set d = SupMap L; now__::_thesis:_for_I_being_Element_of_(InclPoset_(Ids_L)) for_x_being_Element_of_L_holds_ (_(_I_<=_(IdsMap_L)_._x_implies_(SupMap_L)_._I_<=_x_)_&_(_(SupMap_L)_._I_<=_x_implies_I_<=_(IdsMap_L)_._x_)_) let I be Element of (InclPoset (Ids L)); ::_thesis: for x being Element of L holds ( ( I <= (IdsMap L) . x implies (SupMap L) . I <= x ) & ( (SupMap L) . I <= x implies I <= (IdsMap L) . x ) ) let x be Element of L; ::_thesis: ( ( I <= (IdsMap L) . x implies (SupMap L) . I <= x ) & ( (SupMap L) . I <= x implies I <= (IdsMap L) . x ) ) reconsider I9 = I as Ideal of L by YELLOW_2:41; hereby ::_thesis: ( (SupMap L) . I <= x implies I <= (IdsMap L) . x ) assume I <= (IdsMap L) . x ; ::_thesis: (SupMap L) . I <= x then I c= (IdsMap L) . x by YELLOW_1:3; then I9 c= downarrow x by YELLOW_2:def_4; then x is_>=_than I9 by YELLOW_2:1; then sup I9 <= x by YELLOW_0:32; hence (SupMap L) . I <= x by YELLOW_2:def_3; ::_thesis: verum end; assume (SupMap L) . I <= x ; ::_thesis: I <= (IdsMap L) . x then A1: sup I9 <= x by YELLOW_2:def_3; sup I9 is_>=_than I9 by YELLOW_0:32; then x is_>=_than I9 by A1, YELLOW_0:4; then I9 c= downarrow x by YELLOW_2:1; then I c= (IdsMap L) . x by YELLOW_2:def_4; hence I <= (IdsMap L) . x by YELLOW_1:3; ::_thesis: verum end; hence [(IdsMap L),(SupMap L)] is Galois by Th8; ::_thesis: SupMap L is sups-preserving then SupMap L is lower_adjoint by Th9; hence SupMap L is sups-preserving ; ::_thesis: verum end; theorem :: WAYBEL_1:58 for L being non empty complete Poset holds ( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic ) proof let L be non empty complete Poset; ::_thesis: ( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic ) set i = (IdsMap L) * (SupMap L); A1: now__::_thesis:_for_I_being_Ideal_of_L_holds_((IdsMap_L)_*_(SupMap_L))_._I_=_downarrow_(sup_I) let I be Ideal of L; ::_thesis: ((IdsMap L) * (SupMap L)) . I = downarrow (sup I) I is Element of (InclPoset (Ids L)) by YELLOW_2:41; hence ((IdsMap L) * (SupMap L)) . I = (IdsMap L) . ((SupMap L) . I) by FUNCT_2:15 .= (IdsMap L) . (sup I) by YELLOW_2:def_3 .= downarrow (sup I) by YELLOW_2:def_4 ; ::_thesis: verum end; ( (IdsMap L) * (SupMap L) is monotone & [(IdsMap L),(SupMap L)] is Galois ) by Th57, YELLOW_2:12; hence (IdsMap L) * (SupMap L) is closure by Th38; ::_thesis: Image ((IdsMap L) * (SupMap L)),L are_isomorphic take f = (SupMap L) * (inclusion ((IdsMap L) * (SupMap L))); :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic A2: now__::_thesis:_for_x_being_Element_of_(Image_((IdsMap_L)_*_(SupMap_L))) for_I_being_Ideal_of_L_st_x_=_I_holds_ f_._I_=_sup_I let x be Element of (Image ((IdsMap L) * (SupMap L))); ::_thesis: for I being Ideal of L st x = I holds f . I = sup I let I be Ideal of L; ::_thesis: ( x = I implies f . I = sup I ) assume A3: x = I ; ::_thesis: f . I = sup I hence f . I = (SupMap L) . ((inclusion ((IdsMap L) * (SupMap L))) . I) by FUNCT_2:15 .= (SupMap L) . I by A3, FUNCT_1:18 .= sup I by YELLOW_2:def_3 ; ::_thesis: verum end; A4: f is monotone by YELLOW_2:12; A5: now__::_thesis:_for_x,_y_being_Element_of_(Image_((IdsMap_L)_*_(SupMap_L)))_holds_ (_(_x_<=_y_implies_f_._x_<=_f_._y_)_&_(_f_._x_<=_f_._y_implies_x_<=_y_)_) let x, y be Element of (Image ((IdsMap L) * (SupMap L))); ::_thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) consider Ix being Element of (InclPoset (Ids L)) such that A6: ((IdsMap L) * (SupMap L)) . Ix = x by YELLOW_2:10; thus ( x <= y implies f . x <= f . y ) by A4, Def2; ::_thesis: ( f . x <= f . y implies x <= y ) assume A7: f . x <= f . y ; ::_thesis: x <= y ( x is Element of (InclPoset (Ids L)) & y is Element of (InclPoset (Ids L)) ) by YELLOW_0:58; then reconsider x9 = x, y9 = y as Ideal of L by YELLOW_2:41; consider Iy being Element of (InclPoset (Ids L)) such that A8: ((IdsMap L) * (SupMap L)) . Iy = y by YELLOW_2:10; reconsider Ix = Ix, Iy = Iy as Ideal of L by YELLOW_2:41; reconsider i1 = downarrow (sup Ix), i2 = downarrow (sup Iy) as Element of (InclPoset (Ids L)) by YELLOW_2:41; A9: ( ((IdsMap L) * (SupMap L)) . Ix = downarrow (sup Ix) & ((IdsMap L) * (SupMap L)) . Iy = downarrow (sup Iy) ) by A1; A10: ( f . x9 = sup x9 & f . y9 = sup y9 ) by A2; ( sup (downarrow (sup Ix)) = sup Ix & sup (downarrow (sup Iy)) = sup Iy ) by WAYBEL_0:34; then downarrow (sup Ix) c= downarrow (sup Iy) by A7, A6, A8, A9, A10, WAYBEL_0:21; then i1 <= i2 by YELLOW_1:3; hence x <= y by A6, A8, A9, YELLOW_0:60; ::_thesis: verum end; A11: rng f = the carrier of L proof thus rng f c= the carrier of L ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of L c= rng f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of L or x in rng f ) assume x in the carrier of L ; ::_thesis: x in rng f then reconsider x = x as Element of L ; A12: (SupMap L) . (downarrow x) = sup (downarrow x) by YELLOW_2:def_3 .= x by WAYBEL_0:34 ; A13: downarrow x is Element of (InclPoset (Ids L)) by YELLOW_2:41; then ((IdsMap L) * (SupMap L)) . (downarrow x) = (IdsMap L) . ((SupMap L) . (downarrow x)) by FUNCT_2:15 .= downarrow x by A12, YELLOW_2:def_4 ; then downarrow x in rng ((IdsMap L) * (SupMap L)) by A13, FUNCT_2:4; then A14: downarrow x in the carrier of (Image ((IdsMap L) * (SupMap L))) by YELLOW_0:def_15; then f . (downarrow x) = (SupMap L) . ((inclusion ((IdsMap L) * (SupMap L))) . (downarrow x)) by FUNCT_2:15 .= (SupMap L) . (downarrow x) by A14, FUNCT_1:18 ; hence x in rng f by A12, A14, FUNCT_2:4; ::_thesis: verum end; f is V13() proof let x, y be Element of (Image ((IdsMap L) * (SupMap L))); :: according to WAYBEL_1:def_1 ::_thesis: ( f . x = f . y implies x = y ) assume A15: f . x = f . y ; ::_thesis: x = y consider Ix being Element of (InclPoset (Ids L)) such that A16: ((IdsMap L) * (SupMap L)) . Ix = x by YELLOW_2:10; consider Iy being Element of (InclPoset (Ids L)) such that A17: ((IdsMap L) * (SupMap L)) . Iy = y by YELLOW_2:10; ( x is Element of (InclPoset (Ids L)) & y is Element of (InclPoset (Ids L)) ) by YELLOW_0:58; then reconsider x = x, y = y as Ideal of L by YELLOW_2:41; reconsider Ix = Ix, Iy = Iy as Ideal of L by YELLOW_2:41; A18: sup (downarrow (sup Ix)) = sup Ix by WAYBEL_0:34; A19: ( ((IdsMap L) * (SupMap L)) . Ix = downarrow (sup Ix) & ((IdsMap L) * (SupMap L)) . Iy = downarrow (sup Iy) ) by A1; ( f . x = sup x & f . y = sup y ) by A2; hence x = y by A15, A16, A17, A19, A18, WAYBEL_0:34; ::_thesis: verum end; hence f is isomorphic by A11, A5, WAYBEL_0:66; ::_thesis: verum end; definition let S be non empty RelStr ; let x be Element of S; funcx "/\" -> Function of S,S means :Def18: :: WAYBEL_1:def 18 for s being Element of S holds it . s = x "/\" s; existence ex b1 being Function of S,S st for s being Element of S holds b1 . s = x "/\" s proof deffunc H1( Element of S) -> M2( the carrier of S) = x "/\" $1; thus ex f being Function of S,S st for x being Element of S holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of S,S st ( for s being Element of S holds b1 . s = x "/\" s ) & ( for s being Element of S holds b2 . s = x "/\" s ) holds b1 = b2 proof let f1, f2 be Function of S,S; ::_thesis: ( ( for s being Element of S holds f1 . s = x "/\" s ) & ( for s being Element of S holds f2 . s = x "/\" s ) implies f1 = f2 ) assume that A1: for s being Element of S holds f1 . s = x "/\" s and A2: for s being Element of S holds f2 . s = x "/\" s ; ::_thesis: f1 = f2 now__::_thesis:_for_s_being_Element_of_S_holds_f1_._s_=_f2_._s let s be Element of S; ::_thesis: f1 . s = f2 . s thus f1 . s = x "/\" s by A1 .= f2 . s by A2 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def18 defines "/\" WAYBEL_1:def_18_:_ for S being non empty RelStr for x being Element of S for b3 being Function of S,S holds ( b3 = x "/\" iff for s being Element of S holds b3 . s = x "/\" s ); theorem Th59: :: WAYBEL_1:59 for S being non empty RelStr for x, t being Element of S holds { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) proof let S be non empty RelStr ; ::_thesis: for x, t being Element of S holds { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) let x, t be Element of S; ::_thesis: { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (x "/\") " (downarrow t) c= { s where s is Element of S : x "/\" s <= t } let a be set ; ::_thesis: ( a in { s where s is Element of S : x "/\" s <= t } implies a in (x "/\") " (downarrow t) ) assume a in { s where s is Element of S : x "/\" s <= t } ; ::_thesis: a in (x "/\") " (downarrow t) then consider s being Element of S such that A1: a = s and A2: x "/\" s <= t ; (x "/\") . s <= t by A2, Def18; then (x "/\") . s in downarrow t by WAYBEL_0:17; hence a in (x "/\") " (downarrow t) by A1, FUNCT_2:38; ::_thesis: verum end; let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in (x "/\") " (downarrow t) or s in { s where s is Element of S : x "/\" s <= t } ) assume A3: s in (x "/\") " (downarrow t) ; ::_thesis: s in { s where s is Element of S : x "/\" s <= t } then reconsider s = s as Element of S ; (x "/\") . s in downarrow t by A3, FUNCT_2:38; then x "/\" s in downarrow t by Def18; then x "/\" s <= t by WAYBEL_0:17; hence s in { s where s is Element of S : x "/\" s <= t } ; ::_thesis: verum end; theorem Th60: :: WAYBEL_1:60 for S being Semilattice for x being Element of S holds x "/\" is monotone proof let S be Semilattice; ::_thesis: for x being Element of S holds x "/\" is monotone let x be Element of S; ::_thesis: x "/\" is monotone let s1, s2 be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies (x "/\") . s1 <= (x "/\") . s2 ) assume A1: s1 <= s2 ; ::_thesis: (x "/\") . s1 <= (x "/\") . s2 A2: ex_inf_of {x,s1},S by YELLOW_0:21; then A3: x "/\" s1 <= x by YELLOW_0:19; x "/\" s1 <= s1 by A2, YELLOW_0:19; then ( ex_inf_of {x,s2},S & x "/\" s1 <= s2 ) by A1, ORDERS_2:3, YELLOW_0:21; then x "/\" s1 <= x "/\" s2 by A3, YELLOW_0:19; then (x "/\") . s1 <= x "/\" s2 by Def18; hence (x "/\") . s1 <= (x "/\") . s2 by Def18; ::_thesis: verum end; registration let S be Semilattice; let x be Element of S; clusterx "/\" -> monotone ; coherence x "/\" is monotone by Th60; end; theorem Th61: :: WAYBEL_1:61 for S being non empty RelStr for x being Element of S for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X } proof let S be non empty RelStr ; ::_thesis: for x being Element of S for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X } let x be Element of S; ::_thesis: for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X } let X be Subset of S; ::_thesis: (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X } set Y = { (x "/\" y) where y is Element of S : y in X } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (x "/\" y) where y is Element of S : y in X } c= (x "/\") .: X let y be set ; ::_thesis: ( y in (x "/\") .: X implies y in { (x "/\" y) where y is Element of S : y in X } ) assume y in (x "/\") .: X ; ::_thesis: y in { (x "/\" y) where y is Element of S : y in X } then consider z being set such that A1: z in the carrier of S and A2: z in X and A3: y = (x "/\") . z by FUNCT_2:64; reconsider z = z as Element of S by A1; y = x "/\" z by A3, Def18; hence y in { (x "/\" y) where y is Element of S : y in X } by A2; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (x "/\" y) where y is Element of S : y in X } or y in (x "/\") .: X ) assume y in { (x "/\" y) where y is Element of S : y in X } ; ::_thesis: y in (x "/\") .: X then consider z being Element of S such that A4: y = x "/\" z and A5: z in X ; y = (x "/\") . z by A4, Def18; hence y in (x "/\") .: X by A5, FUNCT_2:35; ::_thesis: verum end; theorem Th62: :: WAYBEL_1:62 for S being Semilattice holds ( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ) proof let S be Semilattice; ::_thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ) hereby ::_thesis: ( ( for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ) implies for x being Element of S holds x "/\" is lower_adjoint ) assume A1: for x being Element of S holds x "/\" is lower_adjoint ; ::_thesis: for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S let x, t be Element of S; ::_thesis: ex_max_of { s where s is Element of S : x "/\" s <= t } ,S x "/\" is lower_adjoint by A1; then consider g being Function of S,S such that A2: [g,(x "/\")] is Galois by Def12; set X = { s where s is Element of S : x "/\" s <= t } ; A3: { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) by Th59; g . t is_maximum_of (x "/\") " (downarrow t) by A2, Th11; then ( ex_sup_of { s where s is Element of S : x "/\" s <= t } ,S & "\/" ( { s where s is Element of S : x "/\" s <= t } ,S) in { s where s is Element of S : x "/\" s <= t } ) by A3, Def7; hence ex_max_of { s where s is Element of S : x "/\" s <= t } ,S by Def5; ::_thesis: verum end; assume A4: for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ; ::_thesis: for x being Element of S holds x "/\" is lower_adjoint let x be Element of S; ::_thesis: x "/\" is lower_adjoint deffunc H1( Element of S) -> M2( the carrier of S) = "\/" (((x "/\") " (downarrow $1)),S); consider g being Function of S,S such that A5: for s being Element of S holds g . s = H1(s) from FUNCT_2:sch_4(); now__::_thesis:_for_t_being_Element_of_S_holds_g_._t_is_maximum_of_(x_"/\")_"_(downarrow_t) let t be Element of S; ::_thesis: g . t is_maximum_of (x "/\") " (downarrow t) set X = { s where s is Element of S : x "/\" s <= t } ; ex_max_of { s where s is Element of S : x "/\" s <= t } ,S by A4; then A6: ( ex_sup_of { s where s is Element of S : x "/\" s <= t } ,S & "\/" ( { s where s is Element of S : x "/\" s <= t } ,S) in { s where s is Element of S : x "/\" s <= t } ) by Def5; ( { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) & g . t = "\/" (((x "/\") " (downarrow t)),S) ) by A5, Th59; hence g . t is_maximum_of (x "/\") " (downarrow t) by A6, Def7; ::_thesis: verum end; then [g,(x "/\")] is Galois by Th11; hence x "/\" is lower_adjoint by Def12; ::_thesis: verum end; theorem Th63: :: WAYBEL_1:63 for S being Semilattice st ( for x being Element of S holds x "/\" is lower_adjoint ) holds for X being Subset of S st ex_sup_of X,S holds for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) proof let S be Semilattice; ::_thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) implies for X being Subset of S st ex_sup_of X,S holds for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) assume A1: for x being Element of S holds x "/\" is lower_adjoint ; ::_thesis: for X being Subset of S st ex_sup_of X,S holds for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) let X be Subset of S; ::_thesis: ( ex_sup_of X,S implies for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) assume A2: ex_sup_of X,S ; ::_thesis: for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) let x be Element of S; ::_thesis: x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) x "/\" is sups-preserving by A1, Th13; then x "/\" preserves_sup_of X by WAYBEL_0:def_33; then sup ((x "/\") .: X) = (x "/\") . (sup X) by A2, WAYBEL_0:def_31; hence x "/\" ("\/" (X,S)) = sup ((x "/\") .: X) by Def18 .= "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) by Th61 ; ::_thesis: verum end; theorem :: WAYBEL_1:64 for S being non empty complete Poset holds ( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for X being Subset of S for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) proof let S be non empty complete Poset; ::_thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for X being Subset of S for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) thus ( ( for x being Element of S holds x "/\" is lower_adjoint ) implies for X being Subset of S for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) by Th63, YELLOW_0:17; ::_thesis: ( ( for X being Subset of S for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) implies for x being Element of S holds x "/\" is lower_adjoint ) assume A1: for X being Subset of S for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ; ::_thesis: for x being Element of S holds x "/\" is lower_adjoint let x be Element of S; ::_thesis: x "/\" is lower_adjoint x "/\" is sups-preserving proof let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: x "/\" preserves_sup_of X assume ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (x "/\") .: X,S & "\/" (((x "/\") .: X),S) = (x "/\") . ("\/" (X,S)) ) thus ex_sup_of (x "/\") .: X,S by YELLOW_0:17; ::_thesis: "\/" (((x "/\") .: X),S) = (x "/\") . ("\/" (X,S)) thus (x "/\") . (sup X) = x "/\" ("\/" (X,S)) by Def18 .= "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) by A1 .= sup ((x "/\") .: X) by Th61 ; ::_thesis: verum end; hence x "/\" is lower_adjoint by Th17; ::_thesis: verum end; theorem Th65: :: WAYBEL_1:65 for S being LATTICE st ( for X being Subset of S st ex_sup_of X,S holds for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) holds S is distributive proof let S be LATTICE; ::_thesis: ( ( for X being Subset of S st ex_sup_of X,S holds for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) implies S is distributive ) assume A1: for X being Subset of S st ex_sup_of X,S holds for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ; ::_thesis: S is distributive let x, y, z be Element of S; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) set Y = { (x "/\" s) where s is Element of S : s in {y,z} } ; A2: ex_sup_of {y,z},S by YELLOW_0:20; now__::_thesis:_for_t_being_set_holds_ (_(_not_t_in__{__(x_"/\"_s)_where_s_is_Element_of_S_:_s_in_{y,z}__}__or_t_=_x_"/\"_y_or_t_=_x_"/\"_z_)_&_(_(_t_=_x_"/\"_y_or_t_=_x_"/\"_z_)_implies_t_in__{__(x_"/\"_s)_where_s_is_Element_of_S_:_s_in_{y,z}__}__)_) let t be set ; ::_thesis: ( ( not t in { (x "/\" s) where s is Element of S : s in {y,z} } or t = x "/\" y or t = x "/\" z ) & ( ( t = x "/\" y or t = x "/\" z ) implies b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} } ) ) hereby ::_thesis: ( ( t = x "/\" y or t = x "/\" z ) implies b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} } ) assume t in { (x "/\" s) where s is Element of S : s in {y,z} } ; ::_thesis: ( t = x "/\" y or t = x "/\" z ) then ex s being Element of S st ( t = x "/\" s & s in {y,z} ) ; hence ( t = x "/\" y or t = x "/\" z ) by TARSKI:def_2; ::_thesis: verum end; assume A3: ( t = x "/\" y or t = x "/\" z ) ; ::_thesis: b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} } percases ( t = x "/\" y or t = x "/\" z ) by A3; supposeA4: t = x "/\" y ; ::_thesis: b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} } y in {y,z} by TARSKI:def_2; hence t in { (x "/\" s) where s is Element of S : s in {y,z} } by A4; ::_thesis: verum end; supposeA5: t = x "/\" z ; ::_thesis: b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} } z in {y,z} by TARSKI:def_2; hence t in { (x "/\" s) where s is Element of S : s in {y,z} } by A5; ::_thesis: verum end; end; end; then A6: { (x "/\" s) where s is Element of S : s in {y,z} } = {(x "/\" y),(x "/\" z)} by TARSKI:def_2; thus x "/\" (y "\/" z) = x "/\" (sup {y,z}) by YELLOW_0:41 .= "\/" ({(x "/\" y),(x "/\" z)},S) by A1, A6, A2 .= (x "/\" y) "\/" (x "/\" z) by YELLOW_0:41 ; ::_thesis: verum end; definition let H be non empty RelStr ; attrH is Heyting means :Def19: :: WAYBEL_1:def 19 ( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) ); end; :: deftheorem Def19 defines Heyting WAYBEL_1:def_19_:_ for H being non empty RelStr holds ( H is Heyting iff ( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) ) ); registration cluster non empty Heyting -> non empty reflexive transitive antisymmetric with_suprema with_infima for RelStr ; coherence for b1 being non empty RelStr st b1 is Heyting holds ( b1 is with_infima & b1 is with_suprema & b1 is reflexive & b1 is transitive & b1 is antisymmetric ) by Def19; end; definition let H be non empty RelStr ; let a be Element of H; assume A1: H is Heyting ; funca => -> Function of H,H means :Def20: :: WAYBEL_1:def 20 [it,(a "/\")] is Galois ; existence ex b1 being Function of H,H st [b1,(a "/\")] is Galois proof a "/\" is lower_adjoint by A1, Def19; hence ex b1 being Function of H,H st [b1,(a "/\")] is Galois by Def12; ::_thesis: verum end; uniqueness for b1, b2 being Function of H,H st [b1,(a "/\")] is Galois & [b2,(a "/\")] is Galois holds b1 = b2 proof let g1, g2 be Function of H,H; ::_thesis: ( [g1,(a "/\")] is Galois & [g2,(a "/\")] is Galois implies g1 = g2 ) assume that A2: [g1,(a "/\")] is Galois and A3: [g2,(a "/\")] is Galois ; ::_thesis: g1 = g2 now__::_thesis:_for_x_being_Element_of_H_holds_g1_._x_=_g2_._x let x be Element of H; ::_thesis: g1 . x = g2 . x g1 . x is_maximum_of (a "/\") " (downarrow x) by A1, A2, Th11; then A4: g1 . x = "\/" (((a "/\") " (downarrow x)),H) by Def7; g2 . x is_maximum_of (a "/\") " (downarrow x) by A1, A3, Th11; hence g1 . x = g2 . x by A4, Def7; ::_thesis: verum end; hence g1 = g2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def20 defines => WAYBEL_1:def_20_:_ for H being non empty RelStr for a being Element of H st H is Heyting holds for b3 being Function of H,H holds ( b3 = a => iff [b3,(a "/\")] is Galois ); theorem Th66: :: WAYBEL_1:66 for H being non empty RelStr st H is Heyting holds H is distributive proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies H is distributive ) assume that A1: H is LATTICE and A2: for x being Element of H holds x "/\" is lower_adjoint ; :: according to WAYBEL_1:def_19 ::_thesis: H is distributive for X being Subset of H st ex_sup_of X,H holds for x being Element of H holds x "/\" ("\/" (X,H)) = "\/" ( { (x "/\" y) where y is Element of H : y in X } ,H) by A1, A2, Th63; hence H is distributive by A1, Th65; ::_thesis: verum end; registration cluster non empty Heyting -> non empty distributive for RelStr ; coherence for b1 being non empty RelStr st b1 is Heyting holds b1 is distributive by Th66; end; definition let H be non empty RelStr ; let a, y be Element of H; funca => y -> Element of H equals :: WAYBEL_1:def 21 (a =>) . y; correctness coherence (a =>) . y is Element of H; ; end; :: deftheorem defines => WAYBEL_1:def_21_:_ for H being non empty RelStr for a, y being Element of H holds a => y = (a =>) . y; theorem Th67: :: WAYBEL_1:67 for H being non empty RelStr st H is Heyting holds for x, a, y being Element of H holds ( x >= a "/\" y iff a => x >= y ) proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for x, a, y being Element of H holds ( x >= a "/\" y iff a => x >= y ) ) assume A1: H is Heyting ; ::_thesis: for x, a, y being Element of H holds ( x >= a "/\" y iff a => x >= y ) let x, a, y be Element of H; ::_thesis: ( x >= a "/\" y iff a => x >= y ) [(a =>),(a "/\")] is Galois by A1, Def20; then ( x >= (a "/\") . y iff (a =>) . x >= y ) by A1, Th8; hence ( x >= a "/\" y iff a => x >= y ) by Def18; ::_thesis: verum end; theorem Th68: :: WAYBEL_1:68 for H being non empty RelStr st H is Heyting holds H is upper-bounded proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies H is upper-bounded ) assume A1: H is Heyting ; ::_thesis: H is upper-bounded set a = the Element of H; take the Element of H => the Element of H ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of H is_<=_than the Element of H => the Element of H let y be Element of H; :: according to LATTICE3:def_9 ::_thesis: ( not y in the carrier of H or y <= the Element of H => the Element of H ) assume y in the carrier of H ; ::_thesis: y <= the Element of H => the Element of H the Element of H >= the Element of H "/\" y by A1, YELLOW_0:23; hence y <= the Element of H => the Element of H by A1, Th67; ::_thesis: verum end; registration cluster non empty Heyting -> non empty upper-bounded for RelStr ; coherence for b1 being non empty RelStr st b1 is Heyting holds b1 is upper-bounded by Th68; end; theorem Th69: :: WAYBEL_1:69 for H being non empty RelStr st H is Heyting holds for a, b being Element of H holds ( Top H = a => b iff a <= b ) proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds ( Top H = a => b iff a <= b ) ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds ( Top H = a => b iff a <= b ) let a, b be Element of H; ::_thesis: ( Top H = a => b iff a <= b ) A2: a "/\" (Top H) = (Top H) "/\" a by A1, LATTICE3:15 .= a by A1, Th4 ; hereby ::_thesis: ( a <= b implies Top H = a => b ) assume Top H = a => b ; ::_thesis: a <= b then a => b >= Top H by A1, ORDERS_2:1; hence a <= b by A1, A2, Th67; ::_thesis: verum end; assume a <= b ; ::_thesis: Top H = a => b then A3: a => b >= Top H by A1, A2, Th67; a => b <= Top H by A1, YELLOW_0:45; hence Top H = a => b by A1, A3, ORDERS_2:2; ::_thesis: verum end; theorem :: WAYBEL_1:70 for H being non empty RelStr st H is Heyting holds for a being Element of H holds Top H = a => a proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a being Element of H holds Top H = a => a ) assume A1: H is Heyting ; ::_thesis: for a being Element of H holds Top H = a => a let a be Element of H; ::_thesis: Top H = a => a a >= a "/\" (Top H) by A1, YELLOW_0:23; then A2: Top H <= a => a by A1, Th67; Top H >= a => a by A1, YELLOW_0:45; hence Top H = a => a by A1, A2, ORDERS_2:2; ::_thesis: verum end; theorem :: WAYBEL_1:71 for H being non empty RelStr st H is Heyting holds for a, b being Element of H st Top H = a => b & Top H = b => a holds a = b proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H st Top H = a => b & Top H = b => a holds a = b ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H st Top H = a => b & Top H = b => a holds a = b let a, b be Element of H; ::_thesis: ( Top H = a => b & Top H = b => a implies a = b ) assume A2: Top H = a => b ; ::_thesis: ( not Top H = b => a or a = b ) assume Top H = b => a ; ::_thesis: a = b then A3: b <= a by A1, Th69; a <= b by A1, A2, Th69; hence a = b by A1, A3, ORDERS_2:2; ::_thesis: verum end; theorem Th72: :: WAYBEL_1:72 for H being non empty RelStr st H is Heyting holds for a, b being Element of H holds b <= a => b proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds b <= a => b ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds b <= a => b let a, b be Element of H; ::_thesis: b <= a => b a "/\" b <= b by A1, YELLOW_0:23; hence b <= a => b by A1, Th67; ::_thesis: verum end; theorem :: WAYBEL_1:73 for H being non empty RelStr st H is Heyting holds for a being Element of H holds Top H = a => (Top H) proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a being Element of H holds Top H = a => (Top H) ) assume A1: H is Heyting ; ::_thesis: for a being Element of H holds Top H = a => (Top H) let a be Element of H; ::_thesis: Top H = a => (Top H) a <= Top H by A1, YELLOW_0:45; hence Top H = a => (Top H) by A1, Th69; ::_thesis: verum end; theorem :: WAYBEL_1:74 for H being non empty RelStr st H is Heyting holds for b being Element of H holds b = (Top H) => b proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for b being Element of H holds b = (Top H) => b ) assume A1: H is Heyting ; ::_thesis: for b being Element of H holds b = (Top H) => b let b be Element of H; ::_thesis: b = (Top H) => b (Top H) => b <= (Top H) => b by A1, ORDERS_2:1; then (Top H) "/\" ((Top H) => b) <= b by A1, Th67; then A2: (Top H) => b <= b by A1, Th4; (Top H) => b >= b by A1, Th72; hence b = (Top H) => b by A1, A2, ORDERS_2:2; ::_thesis: verum end; Lm5: for H being non empty RelStr st H is Heyting holds for a, b being Element of H holds a "/\" (a => b) <= b proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds a "/\" (a => b) <= b ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds a "/\" (a => b) <= b let a, b be Element of H; ::_thesis: a "/\" (a => b) <= b a => b <= a => b by A1, ORDERS_2:1; hence a "/\" (a => b) <= b by A1, Th67; ::_thesis: verum end; theorem Th75: :: WAYBEL_1:75 for H being non empty RelStr st H is Heyting holds for a, b, c being Element of H st a <= b holds b => c <= a => c proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b, c being Element of H st a <= b holds b => c <= a => c ) assume A1: H is Heyting ; ::_thesis: for a, b, c being Element of H st a <= b holds b => c <= a => c let a, b, c be Element of H; ::_thesis: ( a <= b implies b => c <= a => c ) assume a <= b ; ::_thesis: b => c <= a => c then A2: a "/\" (b => c) <= b "/\" (b => c) by A1, Th1; b "/\" (b => c) <= c by A1, Lm5; then a "/\" (b => c) <= c by A1, A2, ORDERS_2:3; hence b => c <= a => c by A1, Th67; ::_thesis: verum end; theorem :: WAYBEL_1:76 for H being non empty RelStr st H is Heyting holds for a, b, c being Element of H st b <= c holds a => b <= a => c proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b, c being Element of H st b <= c holds a => b <= a => c ) assume A1: H is Heyting ; ::_thesis: for a, b, c being Element of H st b <= c holds a => b <= a => c let a, b, c be Element of H; ::_thesis: ( b <= c implies a => b <= a => c ) assume A2: b <= c ; ::_thesis: a => b <= a => c a "/\" (a => b) <= b by A1, Lm5; then a "/\" (a => b) <= c by A1, A2, ORDERS_2:3; hence a => b <= a => c by A1, Th67; ::_thesis: verum end; theorem Th77: :: WAYBEL_1:77 for H being non empty RelStr st H is Heyting holds for a, b being Element of H holds a "/\" (a => b) = a "/\" b proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds a "/\" (a => b) = a "/\" b ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds a "/\" (a => b) = a "/\" b let a, b be Element of H; ::_thesis: a "/\" (a => b) = a "/\" b (a "/\" (a => b)) "/\" a <= b "/\" a by A1, Lm5, Th1; then a "/\" (a "/\" (a => b)) <= b "/\" a by A1, LATTICE3:15; then a "/\" (a "/\" (a => b)) <= a "/\" b by A1, LATTICE3:15; then (a "/\" a) "/\" (a => b) <= a "/\" b by A1, LATTICE3:16; then A2: a "/\" (a => b) <= a "/\" b by A1, YELLOW_0:25; b "/\" a <= (a => b) "/\" a by A1, Th1, Th72; then a "/\" b <= (a => b) "/\" a by A1, LATTICE3:15; then a "/\" b <= a "/\" (a => b) by A1, LATTICE3:15; hence a "/\" (a => b) = a "/\" b by A1, A2, ORDERS_2:2; ::_thesis: verum end; theorem Th78: :: WAYBEL_1:78 for H being non empty RelStr st H is Heyting holds for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c) proof let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c) ) assume A1: H is Heyting ; ::_thesis: for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c) let a, b, c be Element of H; ::_thesis: (a "\/" b) => c = (a => c) "/\" (b => c) ( (a "/\" c) "/\" (b => c) <= a "/\" c & a "/\" c <= c ) by A1, YELLOW_0:23; then A2: (a "/\" c) "/\" (b => c) <= c by A1, ORDERS_2:3; ( (b "/\" c) "/\" (a => c) <= b "/\" c & b "/\" c <= c ) by A1, YELLOW_0:23; then A3: (b "/\" c) "/\" (a => c) <= c by A1, ORDERS_2:3; set d = (a => c) "/\" (b => c); (a "\/" b) "/\" ((a => c) "/\" (b => c)) = ((a => c) "/\" (b => c)) "/\" (a "\/" b) by A1, LATTICE3:15 .= (((a => c) "/\" (b => c)) "/\" a) "\/" (((a => c) "/\" (b => c)) "/\" b) by A1, Def3 .= (a "/\" ((a => c) "/\" (b => c))) "\/" (((a => c) "/\" (b => c)) "/\" b) by A1, LATTICE3:15 .= (a "/\" ((a => c) "/\" (b => c))) "\/" (b "/\" ((a => c) "/\" (b => c))) by A1, LATTICE3:15 .= ((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((a => c) "/\" (b => c))) by A1, LATTICE3:16 .= ((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((b => c) "/\" (a => c))) by A1, LATTICE3:15 .= ((a "/\" (a => c)) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c)) by A1, LATTICE3:16 .= ((a "/\" c) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c)) by A1, Th77 .= ((a "/\" c) "/\" (b => c)) "\/" ((b "/\" c) "/\" (a => c)) by A1, Th77 ; then (a "\/" b) "/\" ((a => c) "/\" (b => c)) <= c by A1, A2, A3, YELLOW_0:22; then A4: (a "\/" b) => c >= (a => c) "/\" (b => c) by A1, Th67; b <= a "\/" b by A1, YELLOW_0:22; then A5: (a "\/" b) => c <= b => c by A1, Th75; a <= a "\/" b by A1, YELLOW_0:22; then (a "\/" b) => c <= a => c by A1, Th75; then (a "\/" b) => c <= (a => c) "/\" (b => c) by A1, A5, YELLOW_0:23; hence (a "\/" b) => c = (a => c) "/\" (b => c) by A1, A4, ORDERS_2:2; ::_thesis: verum end; definition let H be non empty RelStr ; let a be Element of H; func 'not' a -> Element of H equals :: WAYBEL_1:def 22 a => (Bottom H); correctness coherence a => (Bottom H) is Element of H; ; end; :: deftheorem defines 'not' WAYBEL_1:def_22_:_ for H being non empty RelStr for a being Element of H holds 'not' a = a => (Bottom H); theorem :: WAYBEL_1:79 for H being non empty RelStr st H is Heyting & H is lower-bounded holds for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H } proof let H be non empty RelStr ; ::_thesis: ( H is Heyting & H is lower-bounded implies for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H } ) assume that A1: H is Heyting and A2: H is lower-bounded ; ::_thesis: for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H } let a be Element of H; ::_thesis: 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H } set X = { x where x is Element of H : a "/\" x = Bottom H } ; set Y = { x where x is Element of H : a "/\" x <= Bottom H } ; A3: { x where x is Element of H : a "/\" x = Bottom H } = { x where x is Element of H : a "/\" x <= Bottom H } proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { x where x is Element of H : a "/\" x <= Bottom H } c= { x where x is Element of H : a "/\" x = Bottom H } let y be set ; ::_thesis: ( y in { x where x is Element of H : a "/\" x = Bottom H } implies y in { x where x is Element of H : a "/\" x <= Bottom H } ) assume y in { x where x is Element of H : a "/\" x = Bottom H } ; ::_thesis: y in { x where x is Element of H : a "/\" x <= Bottom H } then consider x being Element of H such that A4: y = x and A5: a "/\" x = Bottom H ; a "/\" x <= Bottom H by A1, A5, ORDERS_2:1; hence y in { x where x is Element of H : a "/\" x <= Bottom H } by A4; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of H : a "/\" x <= Bottom H } or y in { x where x is Element of H : a "/\" x = Bottom H } ) assume y in { x where x is Element of H : a "/\" x <= Bottom H } ; ::_thesis: y in { x where x is Element of H : a "/\" x = Bottom H } then consider x being Element of H such that A6: y = x and A7: a "/\" x <= Bottom H ; Bottom H <= a "/\" x by A1, A2, YELLOW_0:44; then Bottom H = a "/\" x by A1, A7, ORDERS_2:2; hence y in { x where x is Element of H : a "/\" x = Bottom H } by A6; ::_thesis: verum end; A8: now__::_thesis:_for_b_being_Element_of_H_st_b_is_>=_than__{__x_where_x_is_Element_of_H_:_a_"/\"_x_=_Bottom_H__}__holds_ 'not'_a_<=_b a => (Bottom H) <= a => (Bottom H) by A1, ORDERS_2:1; then a "/\" ('not' a) <= Bottom H by A1, Th67; then A9: 'not' a in { x where x is Element of H : a "/\" x = Bottom H } by A3; let b be Element of H; ::_thesis: ( b is_>=_than { x where x is Element of H : a "/\" x = Bottom H } implies 'not' a <= b ) assume b is_>=_than { x where x is Element of H : a "/\" x = Bottom H } ; ::_thesis: 'not' a <= b hence 'not' a <= b by A9, LATTICE3:def_9; ::_thesis: verum end; for x being Element of H holds x "/\" is lower_adjoint by A1, Def19; then A10: ex_max_of { x where x is Element of H : a "/\" x = Bottom H } ,H by A1, A3, Th62; hence ex_sup_of { x where x is Element of H : a "/\" x = Bottom H } ,H by Def5; :: according to WAYBEL_1:def_7 ::_thesis: ( 'not' a = "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) & "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H } ) 'not' a is_>=_than { x where x is Element of H : a "/\" x = Bottom H } proof let b be Element of H; :: according to LATTICE3:def_9 ::_thesis: ( not b in { x where x is Element of H : a "/\" x = Bottom H } or b <= 'not' a ) assume b in { x where x is Element of H : a "/\" x = Bottom H } ; ::_thesis: b <= 'not' a then ex x being Element of H st ( x = b & a "/\" x <= Bottom H ) by A3; hence b <= 'not' a by A1, Th67; ::_thesis: verum end; hence 'not' a = "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) by A1, A8, YELLOW_0:30; ::_thesis: "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H } thus "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H } by A10, Def5; ::_thesis: verum end; theorem Th80: :: WAYBEL_1:80 for H being non empty RelStr st H is Heyting & H is lower-bounded holds ( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H ) proof let H be non empty RelStr ; ::_thesis: ( H is Heyting & H is lower-bounded implies ( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H ) ) assume that A1: H is Heyting and A2: H is lower-bounded ; ::_thesis: ( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H ) (Top H) => (Bottom H) <= (Top H) => (Bottom H) by A1, ORDERS_2:1; then A3: Bottom H >= (Top H) "/\" ('not' (Top H)) by A1, Th67; Bottom H >= (Bottom H) "/\" (Top H) by A1, YELLOW_0:23; then A4: Top H <= (Bottom H) => (Bottom H) by A1, Th67; Bottom H <= (Top H) "/\" ('not' (Top H)) by A1, A2, YELLOW_0:44; then A5: Bottom H = (Top H) "/\" ('not' (Top H)) by A1, A3, ORDERS_2:2; 'not' (Bottom H) <= Top H by A1, YELLOW_0:45; hence Top H = 'not' (Bottom H) by A1, A4, ORDERS_2:2; ::_thesis: 'not' (Top H) = Bottom H 'not' (Top H) <= Top H by A1, YELLOW_0:45; hence 'not' (Top H) = ('not' (Top H)) "/\" (Top H) by A1, YELLOW_0:25 .= Bottom H by A1, A5, LATTICE3:15 ; ::_thesis: verum end; theorem :: WAYBEL_1:81 for H being non empty lower-bounded RelStr st H is Heyting holds for a, b being Element of H holds ( 'not' a >= b iff 'not' b >= a ) proof let H be non empty lower-bounded RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds ( 'not' a >= b iff 'not' b >= a ) ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds ( 'not' a >= b iff 'not' b >= a ) let a, b be Element of H; ::_thesis: ( 'not' a >= b iff 'not' b >= a ) A2: ( Bottom H >= a "/\" b iff a => (Bottom H) >= b ) by A1, Th67; ( Bottom H >= b "/\" a iff b => (Bottom H) >= a ) by A1, Th67; hence ( 'not' a >= b iff 'not' b >= a ) by A1, A2, LATTICE3:15; ::_thesis: verum end; theorem Th82: :: WAYBEL_1:82 for H being non empty lower-bounded RelStr st H is Heyting holds for a, b being Element of H holds ( 'not' a >= b iff a "/\" b = Bottom H ) proof let H be non empty lower-bounded RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds ( 'not' a >= b iff a "/\" b = Bottom H ) ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds ( 'not' a >= b iff a "/\" b = Bottom H ) let a, b be Element of H; ::_thesis: ( 'not' a >= b iff a "/\" b = Bottom H ) hereby ::_thesis: ( a "/\" b = Bottom H implies 'not' a >= b ) assume 'not' a >= b ; ::_thesis: a "/\" b = Bottom H then A2: a "/\" b <= Bottom H by A1, Th67; a "/\" b >= Bottom H by A1, YELLOW_0:44; hence a "/\" b = Bottom H by A1, A2, ORDERS_2:2; ::_thesis: verum end; assume a "/\" b = Bottom H ; ::_thesis: 'not' a >= b then a "/\" b <= Bottom H by A1, ORDERS_2:1; hence 'not' a >= b by A1, Th67; ::_thesis: verum end; theorem :: WAYBEL_1:83 for H being non empty lower-bounded RelStr st H is Heyting holds for a, b being Element of H st a <= b holds 'not' b <= 'not' a proof let H be non empty lower-bounded RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H st a <= b holds 'not' b <= 'not' a ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H st a <= b holds 'not' b <= 'not' a let a, b be Element of H; ::_thesis: ( a <= b implies 'not' b <= 'not' a ) A2: 'not' b >= 'not' b by A1, ORDERS_2:1; assume a <= b ; ::_thesis: 'not' b <= 'not' a then a "/\" ('not' b) = (a "/\" b) "/\" ('not' b) by A1, YELLOW_0:25 .= a "/\" (b "/\" ('not' b)) by A1, LATTICE3:16 .= a "/\" (Bottom H) by A1, A2, Th82 .= (Bottom H) "/\" a by A1, LATTICE3:15 .= Bottom H by A1, Th3 ; hence 'not' b <= 'not' a by A1, Th82; ::_thesis: verum end; theorem :: WAYBEL_1:84 for H being non empty lower-bounded RelStr st H is Heyting holds for a, b being Element of H holds 'not' (a "\/" b) = ('not' a) "/\" ('not' b) by Th78; theorem :: WAYBEL_1:85 for H being non empty lower-bounded RelStr st H is Heyting holds for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) proof let H be non empty lower-bounded RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) ) assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) then A2: Bottom H <= Bottom H by ORDERS_2:1; let a, b be Element of H; ::_thesis: 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) A3: 'not' a <= 'not' a by A1, ORDERS_2:1; A4: 'not' b <= 'not' b by A1, ORDERS_2:1; (a "/\" b) "/\" (('not' a) "\/" ('not' b)) = ((a "/\" b) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' b)) by A1, Def3 .= ((b "/\" a) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' b)) by A1, LATTICE3:15 .= (b "/\" (a "/\" ('not' a))) "\/" ((a "/\" b) "/\" ('not' b)) by A1, LATTICE3:16 .= (b "/\" (a "/\" ('not' a))) "\/" (a "/\" (b "/\" ('not' b))) by A1, LATTICE3:16 .= (b "/\" (Bottom H)) "\/" (a "/\" (b "/\" ('not' b))) by A1, A3, Th82 .= (b "/\" (Bottom H)) "\/" (a "/\" (Bottom H)) by A1, A4, Th82 .= ((Bottom H) "/\" b) "\/" (a "/\" (Bottom H)) by A1, LATTICE3:15 .= ((Bottom H) "/\" b) "\/" ((Bottom H) "/\" a) by A1, LATTICE3:15 .= (Bottom H) "\/" ((Bottom H) "/\" a) by A1, Th3 .= (Bottom H) "\/" (Bottom H) by A1, Th3 .= Bottom H by A1, A2, YELLOW_0:24 ; hence 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) by A1, Th82; ::_thesis: verum end; definition let L be non empty RelStr ; let x, y be Element of L; predy is_a_complement_of x means :Def23: :: WAYBEL_1:def 23 ( x "\/" y = Top L & x "/\" y = Bottom L ); end; :: deftheorem Def23 defines is_a_complement_of WAYBEL_1:def_23_:_ for L being non empty RelStr for x, y being Element of L holds ( y is_a_complement_of x iff ( x "\/" y = Top L & x "/\" y = Bottom L ) ); definition let L be non empty RelStr ; attrL is complemented means :Def24: :: WAYBEL_1:def 24 for x being Element of L ex y being Element of L st y is_a_complement_of x; end; :: deftheorem Def24 defines complemented WAYBEL_1:def_24_:_ for L being non empty RelStr holds ( L is complemented iff for x being Element of L ex y being Element of L st y is_a_complement_of x ); registration let X be set ; cluster BoolePoset X -> complemented ; coherence BoolePoset X is complemented proof let x be Element of (BoolePoset X); :: according to WAYBEL_1:def_24 ::_thesis: ex y being Element of (BoolePoset X) st y is_a_complement_of x A1: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def_2 .= bool X by LATTICE3:def_1 ; then reconsider y = X \ x as Element of (BoolePoset X) by XBOOLE_1:109; take y ; ::_thesis: y is_a_complement_of x thus x "\/" y = x \/ y by YELLOW_1:17 .= X \/ x by XBOOLE_1:39 .= X by A1, XBOOLE_1:12 .= Top (BoolePoset X) by YELLOW_1:19 ; :: according to WAYBEL_1:def_23 ::_thesis: x "/\" y = Bottom (BoolePoset X) A2: x misses y by XBOOLE_1:79; thus x "/\" y = x /\ y by YELLOW_1:17 .= {} by A2, XBOOLE_0:def_7 .= Bottom (BoolePoset X) by YELLOW_1:18 ; ::_thesis: verum end; end; Lm6: for L being bounded LATTICE st L is distributive & L is complemented holds for x being Element of L ex x9 being Element of L st for y being Element of L holds ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) proof let L be bounded LATTICE; ::_thesis: ( L is distributive & L is complemented implies for x being Element of L ex x9 being Element of L st for y being Element of L holds ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) assume that A1: L is distributive and A2: L is complemented ; ::_thesis: for x being Element of L ex x9 being Element of L st for y being Element of L holds ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) let x be Element of L; ::_thesis: ex x9 being Element of L st for y being Element of L holds ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) consider x9 being Element of L such that A3: x9 is_a_complement_of x by A2, Def24; take x9 ; ::_thesis: for y being Element of L holds ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) let y be Element of L; ::_thesis: ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) (y "\/" x9) "/\" x = (x "/\" y) "\/" (x "/\" x9) by A1, Def3 .= (Bottom L) "\/" (x "/\" y) by A3, Def23 .= x "/\" y by Th3 ; hence (y "\/" x9) "/\" x <= y by YELLOW_0:23; ::_thesis: y <= (y "/\" x) "\/" x9 (y "/\" x) "\/" x9 = (x9 "\/" y) "/\" (x9 "\/" x) by A1, Th5 .= (x9 "\/" y) "/\" (Top L) by A3, Def23 .= x9 "\/" y by Th4 ; hence y <= (y "/\" x) "\/" x9 by YELLOW_0:22; ::_thesis: verum end; Lm7: for L being bounded LATTICE st ( for x being Element of L ex x9 being Element of L st for y being Element of L holds ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) holds ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) proof let L be bounded LATTICE; ::_thesis: ( ( for x being Element of L ex x9 being Element of L st for y being Element of L holds ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) implies ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) ) defpred S1[ Element of L, Element of L] means for y being Element of L holds ( (y "\/" $2) "/\" $1 <= y & y <= (y "/\" $1) "\/" $2 ); assume A1: for x being Element of L ex x9 being Element of L st S1[x,x9] ; ::_thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) consider g9 being Function of L,L such that A2: for x being Element of L holds S1[x,g9 . x] from FUNCT_2:sch_3(A1); A3: now__::_thesis:_for_y_being_Element_of_L for_g_being_Function_of_L,L_st_(_for_z_being_Element_of_L_holds_g_._z_=_(g9_._y)_"\/"_z_)_holds_ [g,(y_"/\")]_is_Galois let y be Element of L; ::_thesis: for g being Function of L,L st ( for z being Element of L holds g . z = (g9 . y) "\/" z ) holds [g,(y "/\")] is Galois let g be Function of L,L; ::_thesis: ( ( for z being Element of L holds g . z = (g9 . y) "\/" z ) implies [g,(y "/\")] is Galois ) assume A4: for z being Element of L holds g . z = (g9 . y) "\/" z ; ::_thesis: [g,(y "/\")] is Galois A5: now__::_thesis:_for_x,_z_being_Element_of_L_holds_ (_(_x_<=_g_._z_implies_(y_"/\")_._x_<=_z_)_&_(_(y_"/\")_._x_<=_z_implies_x_<=_g_._z_)_) let x, z be Element of L; ::_thesis: ( ( x <= g . z implies (y "/\") . x <= z ) & ( (y "/\") . x <= z implies x <= g . z ) ) hereby ::_thesis: ( (y "/\") . x <= z implies x <= g . z ) assume x <= g . z ; ::_thesis: (y "/\") . x <= z then x <= (g9 . y) "\/" z by A4; then A6: x "/\" y <= ((g9 . y) "\/" z) "/\" y by Th1; ((g9 . y) "\/" z) "/\" y <= z by A2; then x "/\" y <= z by A6, ORDERS_2:3; hence (y "/\") . x <= z by Def18; ::_thesis: verum end; assume (y "/\") . x <= z ; ::_thesis: x <= g . z then y "/\" x <= z by Def18; then A7: (x "/\" y) "\/" (g9 . y) <= z "\/" (g9 . y) by Th2; x <= (x "/\" y) "\/" (g9 . y) by A2; then x <= z "\/" (g9 . y) by A7, ORDERS_2:3; hence x <= g . z by A4; ::_thesis: verum end; g is monotone proof let z1, z2 be Element of L; :: according to WAYBEL_1:def_2 ::_thesis: ( z1 <= z2 implies g . z1 <= g . z2 ) assume z1 <= z2 ; ::_thesis: g . z1 <= g . z2 then (g9 . y) "\/" z1 <= z2 "\/" (g9 . y) by Th2; then g . z1 <= (g9 . y) "\/" z2 by A4; hence g . z1 <= g . z2 by A4; ::_thesis: verum end; hence [g,(y "/\")] is Galois by A5, Th8; ::_thesis: verum end; thus A8: L is Heyting ::_thesis: for x being Element of L holds 'not' ('not' x) = x proof thus L is LATTICE ; :: according to WAYBEL_1:def_19 ::_thesis: for x being Element of L holds x "/\" is lower_adjoint let y be Element of L; ::_thesis: y "/\" is lower_adjoint deffunc H1( Element of L) -> M2( the carrier of L) = (g9 . y) "\/" $1; consider g being Function of L,L such that A9: for z being Element of L holds g . z = H1(z) from FUNCT_2:sch_4(); [g,(y "/\")] is Galois by A3, A9; hence y "/\" is lower_adjoint by Def12; ::_thesis: verum end; A10: now__::_thesis:_for_x_being_Element_of_L_holds_'not'_x_=_g9_._x let x be Element of L; ::_thesis: 'not' x = g9 . x deffunc H1( Element of L) -> M2( the carrier of L) = (g9 . x) "\/" $1; consider g being Function of L,L such that A11: for z being Element of L holds g . z = H1(z) from FUNCT_2:sch_4(); [g,(x "/\")] is Galois by A3, A11; then g = x => by A8, Def20; hence 'not' x = (Bottom L) "\/" (g9 . x) by A11 .= g9 . x by Th3 ; ::_thesis: verum end; A12: now__::_thesis:_for_x_being_Element_of_L_holds_Bottom_L_=_x_"/\"_('not'_x) let x be Element of L; ::_thesis: Bottom L = x "/\" ('not' x) ((Bottom L) "\/" (g9 . x)) "/\" x <= Bottom L by A2; then (x "/\" (Bottom L)) "\/" (x "/\" (g9 . x)) <= Bottom L by A8, Def3; then (Bottom L) "\/" (x "/\" (g9 . x)) <= Bottom L by Th3; then A13: x "/\" (g9 . x) <= Bottom L by Th3; Bottom L <= x "/\" (g9 . x) by YELLOW_0:44; hence Bottom L = x "/\" (g9 . x) by A13, ORDERS_2:2 .= x "/\" ('not' x) by A10 ; ::_thesis: verum end; let x be Element of L; ::_thesis: 'not' ('not' x) = x A14: now__::_thesis:_for_x_being_Element_of_L_holds_Top_L_=_x_"\/"_('not'_x) let x be Element of L; ::_thesis: Top L = x "\/" ('not' x) Top L <= ((Top L) "/\" x) "\/" (g9 . x) by A2; then A15: Top L <= x "\/" (g9 . x) by Th4; x "\/" (g9 . x) <= Top L by YELLOW_0:45; hence Top L = x "\/" (g9 . x) by A15, ORDERS_2:2 .= x "\/" ('not' x) by A10 ; ::_thesis: verum end; then (('not' x) "\/" ('not' ('not' x))) "/\" x = (Top L) "/\" x ; then x = x "/\" (('not' x) "\/" ('not' ('not' x))) by Th4 .= (x "/\" ('not' x)) "\/" (x "/\" ('not' ('not' x))) by A8, Def3 .= (Bottom L) "\/" (x "/\" ('not' ('not' x))) by A12 .= x "/\" ('not' ('not' x)) by Th3 ; then A16: x <= 'not' ('not' x) by YELLOW_0:25; (Bottom L) "\/" x = (('not' x) "/\" ('not' ('not' x))) "\/" x by A12; then x = x "\/" (('not' x) "/\" ('not' ('not' x))) by Th3 .= (x "\/" ('not' x)) "/\" (x "\/" ('not' ('not' x))) by A8, Th5 .= (Top L) "/\" (x "\/" ('not' ('not' x))) by A14 .= x "\/" ('not' ('not' x)) by Th4 ; hence 'not' ('not' x) = x by A16, YELLOW_0:24; ::_thesis: verum end; theorem Th86: :: WAYBEL_1:86 for L being bounded LATTICE st L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) holds for x being Element of L holds 'not' x is_a_complement_of x proof let L be bounded LATTICE; ::_thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) implies for x being Element of L holds 'not' x is_a_complement_of x ) assume that A1: L is Heyting and A2: for x being Element of L holds 'not' ('not' x) = x ; ::_thesis: for x being Element of L holds 'not' x is_a_complement_of x let x be Element of L; ::_thesis: 'not' x is_a_complement_of x A3: 'not' (x "\/" ('not' x)) = ('not' x) "/\" ('not' ('not' x)) by A1, Th78 .= x "/\" ('not' x) by A2 ; A4: 'not' x >= 'not' x by ORDERS_2:1; then x "/\" ('not' x) = Bottom L by A1, Th82; hence x "\/" ('not' x) = 'not' (Bottom L) by A2, A3 .= Top L by A1, Th80 ; :: according to WAYBEL_1:def_23 ::_thesis: x "/\" ('not' x) = Bottom L thus x "/\" ('not' x) = Bottom L by A1, A4, Th82; ::_thesis: verum end; theorem Th87: :: WAYBEL_1:87 for L being bounded LATTICE holds ( L is distributive & L is complemented iff ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) ) proof let L be bounded LATTICE; ::_thesis: ( L is distributive & L is complemented iff ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) ) hereby ::_thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) implies ( L is distributive & L is complemented ) ) assume ( L is distributive & L is complemented ) ; ::_thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) then for x being Element of L ex x9 being Element of L st for y being Element of L holds ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) by Lm6; hence ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) by Lm7; ::_thesis: verum end; assume that A1: L is Heyting and A2: for x being Element of L holds 'not' ('not' x) = x ; ::_thesis: ( L is distributive & L is complemented ) thus L is distributive by A1; ::_thesis: L is complemented let x be Element of L; :: according to WAYBEL_1:def_24 ::_thesis: ex y being Element of L st y is_a_complement_of x take 'not' x ; ::_thesis: 'not' x is_a_complement_of x thus 'not' x is_a_complement_of x by A1, A2, Th86; ::_thesis: verum end; definition let B be non empty RelStr ; attrB is Boolean means :Def25: :: WAYBEL_1:def 25 ( B is LATTICE & B is bounded & B is distributive & B is complemented ); end; :: deftheorem Def25 defines Boolean WAYBEL_1:def_25_:_ for B being non empty RelStr holds ( B is Boolean iff ( B is LATTICE & B is bounded & B is distributive & B is complemented ) ); registration cluster non empty Boolean -> non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented for RelStr ; coherence for b1 being non empty RelStr st b1 is Boolean holds ( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_infima & b1 is with_suprema & b1 is bounded & b1 is distributive & b1 is complemented ) by Def25; end; registration cluster non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented -> non empty Boolean for RelStr ; coherence for b1 being non empty RelStr st b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_infima & b1 is with_suprema & b1 is bounded & b1 is distributive & b1 is complemented holds b1 is Boolean by Def25; end; registration cluster non empty Boolean -> non empty Heyting for RelStr ; coherence for b1 being non empty RelStr st b1 is Boolean holds b1 is Heyting by Th87; end; registration cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Boolean for RelStr ; existence ex b1 being LATTICE st ( b1 is strict & b1 is Boolean & not b1 is empty ) proof take BoolePoset {} ; ::_thesis: ( BoolePoset {} is strict & BoolePoset {} is Boolean & not BoolePoset {} is empty ) thus ( BoolePoset {} is strict & BoolePoset {} is Boolean & not BoolePoset {} is empty ) ; ::_thesis: verum end; end; registration cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Heyting for RelStr ; existence ex b1 being LATTICE st ( b1 is strict & b1 is Heyting & not b1 is empty ) proof set L = the non empty strict Boolean LATTICE; take the non empty strict Boolean LATTICE ; ::_thesis: ( the non empty strict Boolean LATTICE is strict & the non empty strict Boolean LATTICE is Heyting & not the non empty strict Boolean LATTICE is empty ) thus ( the non empty strict Boolean LATTICE is strict & the non empty strict Boolean LATTICE is Heyting & not the non empty strict Boolean LATTICE is empty ) ; ::_thesis: verum end; end;