:: WAYBEL10 semantic presentation

begin

scheme :: WAYBEL10:sch 1
SubrelstrEx{ F1() ->  non empty RelStr , P1[ set ], F2() ->  set } :
 ex S being non empty strict full SubRelStr of F1() st
for x being Element of F1() holds
( x is Element of S iff P1[x] )
provided
A1: P1[F2()] and
A2: F2() in the carrier of F1()
proof
consider A being set  such that
A3: for x being set holds
( x in A iff ( x in the carrier of F1() & P1[x] ) ) from XBOOLE_0:sch_1();
 A c= the carrier of F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the carrier of F1() )
thus  ( not x in A or x in the carrier of F1() ) by A3; ::_thesis: verum
end;
then reconsider A = A as non empty Subset of F1() by A1, A2, A3;
set S = subrelstr A;
take  subrelstr A ; ::_thesis: for x being Element of F1() holds
( x is Element of (subrelstr A) iff P1[x] )
let x be Element of F1(); ::_thesis: ( x is Element of (subrelstr A) iff P1[x] )
A4: the carrier of (subrelstr A) = A by YELLOW_0:def_15;
hence  ( x is Element of (subrelstr A) implies P1[x] ) by A3; ::_thesis: ( P1[x] implies x is Element of (subrelstr A) )
assume  P1[x] ; ::_thesis: x is Element of (subrelstr A)
hence  x is Element of (subrelstr A) by A3, A4; ::_thesis: verum
end;

scheme :: WAYBEL10:sch 2
RelstrEq{ F1() ->  non empty RelStr , F2() ->  non empty RelStr , P1[ set ], P2[ set , set ] } :
 RelStr(# the carrier of F1(), the InternalRel of F1() #) = RelStr(# the carrier of F2(), the InternalRel of F2() #)
provided
A1: for x being set holds
( x is Element of F1() iff P1[x] ) and
A2: for x being set holds
( x is Element of F2() iff P1[x] ) and
A3: for a, b being Element of F1() holds
( a <= b iff P2[a,b] ) and
A4: for a, b being Element of F2() holds
( a <= b iff P2[a,b] )
proof
set S1 = F1();
set S2 = F2();
A5: the carrier of F1() = the carrier of F2()
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of F2() c= the carrier of F1()
let x be set ; ::_thesis: ( x in the carrier of F1() implies x in the carrier of F2() )
assume  x in the carrier of F1() ; ::_thesis: x in the carrier of F2()
then reconsider y = x as Element of F1() ;
 P1[y] by A1;
then  x is Element of F2() by A2;
hence  x in the carrier of F2() ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of F2() or x in the carrier of F1() )
assume  x in the carrier of F2() ; ::_thesis: x in the carrier of F1()
then reconsider y = x as Element of F2() ;
 P1[y] by A2;
then  x is Element of F1() by A1;
hence  x in the carrier of F1() ; ::_thesis: verum
end;
 the InternalRel of F1() = the InternalRel of F2()
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of F1() or [x,y] in the InternalRel of F2() ) & ( not [x,y] in the InternalRel of F2() or [x,y] in the InternalRel of F1() ) )
hereby  ::_thesis: ( not [x,y] in the InternalRel of F2() or [x,y] in the InternalRel of F1() )
assume A6: [x,y] in the InternalRel of F1() ; ::_thesis: [x,y] in the InternalRel of F2()
then reconsider x1 = x, y1 = y as Element of F1() by ZFMISC_1:87;
reconsider x2 = x1, y2 = y1 as Element of F2() by A5;
 x1 <= y1 by A6, ORDERS_2:def_5;
then  P2[x1,y1] by A3;
then  x2 <= y2 by A4;
hence  [x,y] in the InternalRel of F2() by ORDERS_2:def_5; ::_thesis: verum
end;
assume A7: [x,y] in the InternalRel of F2() ; ::_thesis: [x,y] in the InternalRel of F1()
then reconsider x2 = x, y2 = y as Element of F2() by ZFMISC_1:87;
reconsider x1 = x2, y1 = y2 as Element of F1() by A5;
 x2 <= y2 by A7, ORDERS_2:def_5;
then  P2[x2,y2] by A4;
then  x1 <= y1 by A3;
hence  [x,y] in the InternalRel of F1() by ORDERS_2:def_5; ::_thesis: verum
end;
hence  RelStr(# the carrier of F1(), the InternalRel of F1() #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) by A5; ::_thesis: verum
end;

scheme :: WAYBEL10:sch 3
SubrelstrEq1{ F1() ->  non empty RelStr , F2() ->  non empty full SubRelStr of F1(), F3() ->  non empty full SubRelStr of F1(), P1[ set ] } :
 RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #)
provided
A1: for x being set holds
( x is Element of F2() iff P1[x] ) and
A2: for x being set holds
( x is Element of F3() iff P1[x] )
proof
A3: for x being set holds
( x is Element of F3() iff P1[x] ) by A2;
defpred S1[ set , set ] means [$1,$2] in the InternalRel of F1();
A4: now__::_thesis:_for_a,_b_being_Element_of_F2()_holds_
(_a_<=_b_iff_S1[a,b]_)
let a, b be Element of F2(); ::_thesis: ( a <= b iff S1[a,b] )
reconsider x = a, y = b as Element of F1() by YELLOW_0:58;
 ( x <= y iff [x,y] in the InternalRel of F1() ) by ORDERS_2:def_5;
hence  ( a <= b iff S1[a,b] ) by YELLOW_0:59, YELLOW_0:60; ::_thesis: verum
end;
A5: now__::_thesis:_for_a,_b_being_Element_of_F3()_holds_
(_a_<=_b_iff_S1[a,b]_)
let a, b be Element of F3(); ::_thesis: ( a <= b iff S1[a,b] )
reconsider x = a, y = b as Element of F1() by YELLOW_0:58;
 ( x <= y iff [x,y] in the InternalRel of F1() ) by ORDERS_2:def_5;
hence  ( a <= b iff S1[a,b] ) by YELLOW_0:59, YELLOW_0:60; ::_thesis: verum
end;
A6: for x being set holds
( x is Element of F2() iff P1[x] ) by A1;
thus  RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #) from WAYBEL10:sch_2(A6, A3, A4, A5); ::_thesis: verum
end;

scheme :: WAYBEL10:sch 4
SubrelstrEq2{ F1() ->  non empty RelStr , F2() ->  non empty full SubRelStr of F1(), F3() ->  non empty full SubRelStr of F1(), P1[ set ] } :
 RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #)
provided
A1: for x being Element of F1() holds
( x is Element of F2() iff P1[x] ) and
A2: for x being Element of F1() holds
( x is Element of F3() iff P1[x] )
proof
defpred S1[ set ] means ( P1[$1] & $1 is Element of F1() );
A3: now__::_thesis:_for_x_being_set_holds_
(_x_is_Element_of_F3()_iff_S1[x]_)
let x be set ; ::_thesis: ( x is Element of F3() iff S1[x] )
 ( x is Element of F3() implies x is Element of F1() ) by YELLOW_0:58;
hence  ( x is Element of F3() iff S1[x] ) by A2; ::_thesis: verum
end;
A4: now__::_thesis:_for_x_being_set_holds_
(_x_is_Element_of_F2()_iff_S1[x]_)
let x be set ; ::_thesis: ( x is Element of F2() iff S1[x] )
 ( x is Element of F2() implies x is Element of F1() ) by YELLOW_0:58;
hence  ( x is Element of F2() iff S1[x] ) by A1; ::_thesis: verum
end;
thus  RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #) from WAYBEL10:sch_3(A4, A3); ::_thesis: verum
end;

theorem Th1: :: WAYBEL10:1
for R, Q being Relation holds
( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) )
proof
let R, Q be Relation; ::_thesis: ( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) )
A1: (Q ~) ~ = Q ;
 (R ~) ~ = R ;
hence  ( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) ) by A1, SYSREL:11; ::_thesis: verum
end;

theorem Th2: :: WAYBEL10:2
for L, S being RelStr holds
( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) & ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) )
proof
let L, S be RelStr ; ::_thesis: ( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) & ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) )
thus  ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) ::_thesis: ( ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) )
proof
assume that
A1: the carrier of S c= the carrier of L and
A2: the InternalRel of S c= the InternalRel of L ; :: according to YELLOW_0:def_13 ::_thesis: S opp is SubRelStr of L opp
thus  ( the carrier of (S opp) c= the carrier of (L opp) & the InternalRel of (S opp) c= the InternalRel of (L opp) ) by A1, A2, Th1; :: according to YELLOW_0:def_13 ::_thesis: verum
end;
thus  ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) ::_thesis: ( S opp is SubRelStr of L iff S is SubRelStr of L opp )
proof
assume that
A3: the carrier of (S opp) c= the carrier of (L opp) and
A4: the InternalRel of (S opp) c= the InternalRel of (L opp) ; :: according to YELLOW_0:def_13 ::_thesis: S is SubRelStr of L
thus  ( the carrier of S c= the carrier of L & the InternalRel of S c= the InternalRel of L ) by A3, A4, Th1; :: according to YELLOW_0:def_13 ::_thesis: verum
end;
thus  ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) ::_thesis: ( S is SubRelStr of L opp implies S opp is SubRelStr of L )
proof
assume that
A5: the carrier of (S opp) c= the carrier of L and
A6: the InternalRel of (S opp) c= the InternalRel of L ; :: according to YELLOW_0:def_13 ::_thesis: S is SubRelStr of L opp
thus  ( the carrier of S c= the carrier of (L opp) & the InternalRel of S c= the InternalRel of (L opp) ) by A5, A6, Th1; :: according to YELLOW_0:def_13 ::_thesis: verum
end;
assume that
A7: the carrier of S c= the carrier of (L opp) and
A8: the InternalRel of S c= the InternalRel of (L opp) ; :: according to YELLOW_0:def_13 ::_thesis: S opp is SubRelStr of L
thus  ( the carrier of (S opp) c= the carrier of L & the InternalRel of (S opp) c= the InternalRel of L ) by A7, A8, Th1; :: according to YELLOW_0:def_13 ::_thesis: verum
end;

theorem Th3: :: WAYBEL10:3
for L, S being RelStr holds
( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )
proof
let L, S be RelStr ; ::_thesis: ( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )
A1: ( the InternalRel of L |_2 the carrier of S) ~ = ( the InternalRel of L ~) |_2 the carrier of S by ORDERS_1:83;
hereby  ::_thesis: ( ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )
assume A2: S is full SubRelStr of L ; ::_thesis: S opp is full SubRelStr of L opp
then  the InternalRel of S = the InternalRel of L |_2 the carrier of S by YELLOW_0:def_14;
hence  S opp is full SubRelStr of L opp by A1, A2, Th2, YELLOW_0:def_14; ::_thesis: verum
end;
A3: (( the InternalRel of L ~) |_2 the carrier of S) ~ = (( the InternalRel of L ~) ~) |_2 the carrier of S by ORDERS_1:83;
hereby  ::_thesis: ( S opp is full SubRelStr of L iff S is full SubRelStr of L opp )
assume A4: S opp is full SubRelStr of L opp ; ::_thesis: S is full SubRelStr of L
then  the InternalRel of (S opp) = the InternalRel of (L opp) |_2 the carrier of S by YELLOW_0:def_14;
hence  S is full SubRelStr of L by A3, A4, Th2, YELLOW_0:def_14; ::_thesis: verum
end;
hereby  ::_thesis: ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L )
assume A5: S opp is full SubRelStr of L ; ::_thesis: S is full SubRelStr of L opp
then  the InternalRel of (S opp) = the InternalRel of L |_2 the carrier of S by YELLOW_0:def_14;
hence  S is full SubRelStr of L opp by A1, A5, Th2, YELLOW_0:def_14; ::_thesis: verum
end;
assume A6: S is full SubRelStr of L opp ; ::_thesis: S opp is full SubRelStr of L
then  the InternalRel of S = the InternalRel of (L opp) |_2 the carrier of S by YELLOW_0:def_14;
hence  S opp is full SubRelStr of L by A1, A6, Th2, YELLOW_0:def_14; ::_thesis: verum
end;

definition
let L be RelStr ;
let S be full SubRelStr of L;
:: original: ~
redefine funcS opp  ->  strict full SubRelStr of L opp ;
coherence
 S ~ is strict full SubRelStr of L opp by Th3;
end;

registration
let X be set ;
let L be non empty RelStr ;
clusterX --> L ->  non-Empty ;
coherence
 X --> L is non-Empty
proof
let R be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not R in rng (X --> L) or not R is empty )
assume  R in rng (X --> L) ; ::_thesis: not R is empty
hence  not R is empty by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let S be RelStr ;
let T be non empty reflexive RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V24( the carrier of S) quasi_total monotone for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st b1 is monotone
proof
set c = the Element of T;
take f = S --> the Element of T; ::_thesis: f is monotone
let x, y be Element of S; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
assume  [x,y] in the InternalRel of S ; :: according to ORDERS_2:def_5 ::_thesis: for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )
then A1: x in the carrier of S by ZFMISC_1:87;
let a, b be Element of T; ::_thesis: ( not a = f . x or not b = f . y or a <= b )
assume that
A2: a = f . x and
A3: b = f . y ; ::_thesis: a <= b
 a = the Element of T by A1, A2, FUNCOP_1:7;
hence  a <= b by A1, A3, FUNCOP_1:7; ::_thesis: verum
end;
end;

registration
let L be non empty RelStr ;
cluster Function-like quasi_total projection  ->  idempotent monotone for Element of bool [: the carrier of L, the carrier of L:];
coherence
 for b1 being Function of L,L st b1 is projection holds
( b1 is monotone & b1 is idempotent ) by WAYBEL_1:def_13;
end;

registration
let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
cluster corestr f ->  monotone ;
coherence
 corestr f is monotone
proof
let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (corestr f) . x <= (corestr f) . y )
A1: f . y = (corestr f) . y by WAYBEL_1:30;
assume  x <= y ; ::_thesis: (corestr f) . x <= (corestr f) . y
then A2: f . x <= f . y by WAYBEL_1:def_2;
 f . x = (corestr f) . x by WAYBEL_1:30;
hence  (corestr f) . x <= (corestr f) . y by A2, A1, YELLOW_0:60; ::_thesis: verum
end;
end;

registration
let L be non empty reflexive RelStr ;
cluster id L ->  infs-preserving sups-preserving ;
coherence
 ( id L is sups-preserving & id L is infs-preserving )
proof
thus  id L is sups-preserving ::_thesis: id L is infs-preserving
proof
let X be Subset of L; :: according to WAYBEL_0:def_33 ::_thesis: id L preserves_sup_of X
A1: (id L) . (sup X) = sup X by FUNCT_1:18;
assume  ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (id L) .: X,L & "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) )
hence  ( ex_sup_of (id L) .: X,L & "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) ) by A1, FUNCT_1:92; ::_thesis: verum
end;
let X be Subset of L; :: according to WAYBEL_0:def_32 ::_thesis: id L preserves_inf_of X
A2: (id L) . (inf X) = inf X by FUNCT_1:18;
assume  ex_inf_of X,L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (id L) .: X,L & "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) )
hence  ( ex_inf_of (id L) .: X,L & "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) ) by A2, FUNCT_1:92; ::_thesis: verum
end;
end;

theorem :: WAYBEL10:4
for L being RelStr
for S being Subset of L holds
( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds
f is monotone ) )
proof
let L be RelStr ; ::_thesis: for S being Subset of L holds
( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds
f is monotone ) )
let S be Subset of L; ::_thesis: ( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds
f is monotone ) )
A1: the carrier of (subrelstr S) = S by YELLOW_0:def_15;
A2: rng (id S) = S by RELAT_1:45;
 dom (id S) = S by RELAT_1:45;
hence  id S is Function of (subrelstr S),L by A1, A2, FUNCT_2:2; ::_thesis: for f being Function of (subrelstr S),L st f = id S holds
f is monotone
let f be Function of (subrelstr S),L; ::_thesis: ( f = id S implies f is monotone )
assume A3: f = id S ; ::_thesis: f is monotone
let x, y be Element of (subrelstr S); :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
assume A4: [x,y] in the InternalRel of (subrelstr S) ; :: according to ORDERS_2:def_5 ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )
let a, b be Element of L; ::_thesis: ( not a = f . x or not b = f . y or a <= b )
assume that
A5: a = f . x and
A6: b = f . y ; ::_thesis: a <= b
 x in S by A1, A4, ZFMISC_1:87;
then A7: a = x by A3, A5, FUNCT_1:17;
 y in S by A1, A4, ZFMISC_1:87;
then A8: b = y by A3, A6, FUNCT_1:17;
 the InternalRel of (subrelstr S) c= the InternalRel of L by YELLOW_0:def_13;
hence  [a,b] in the InternalRel of L by A4, A7, A8; :: according to ORDERS_2:def_5 ::_thesis: verum
end;

registration
let L be non empty reflexive RelStr ;
cluster Relation-like the carrier of L -defined the carrier of L -valued Function-like V7() non empty V24( the carrier of L) quasi_total infs-preserving sups-preserving closure kernel for Element of bool [: the carrier of L, the carrier of L:];
existence
 ex b1 being Function of L,L st
( b1 is sups-preserving & b1 is infs-preserving & b1 is closure & b1 is kernel & b1 is V7() )
proof
take  id L ; ::_thesis: ( id L is sups-preserving & id L is infs-preserving & id L is closure & id L is kernel & id L is V7() )
thus  ( id L is sups-preserving & id L is infs-preserving & id L is closure & id L is kernel & id L is V7() ) ; ::_thesis: verum
end;
end;

theorem Th5: :: WAYBEL10:5
for L being non empty reflexive RelStr
for c being closure Function of L,L
for x being Element of L holds c . x >= x
proof
let L be non empty reflexive RelStr ; ::_thesis: for c being closure Function of L,L
for x being Element of L holds c . x >= x
let c be closure Function of L,L; ::_thesis: for x being Element of L holds c . x >= x
let x be Element of L; ::_thesis: c . x >= x
 c >= id L by WAYBEL_1:def_14;
then  c . x >= (id L) . x by YELLOW_2:9;
hence  c . x >= x by FUNCT_1:18; ::_thesis: verum
end;

theorem Th6: :: WAYBEL10:6
for S, T being RelStr
for R being SubRelStr of S
for f being Function of the carrier of S, the carrier of T holds
( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
proof
let S, T be RelStr ; ::_thesis: for R being SubRelStr of S
for f being Function of the carrier of S, the carrier of T holds
( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
let R be SubRelStr of S; ::_thesis: for f being Function of the carrier of S, the carrier of T holds
( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
let f be Function of the carrier of S, the carrier of T; ::_thesis: ( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
 the carrier of R c= the carrier of S by YELLOW_0:def_13;
hence  f | R = f | the carrier of R by TMAP_1:def_3; ::_thesis: for x being set st x in the carrier of R holds
(f | R) . x = f . x
hence  for x being set st x in the carrier of R holds
(f | R) . x = f . x by FUNCT_1:49; ::_thesis: verum
end;

theorem Th7: :: WAYBEL10:7
for S, T being RelStr
for f being Function of S,T st f is one-to-one holds
for R being SubRelStr of S holds f | R is one-to-one
proof
let S, T be RelStr ; ::_thesis: for f being Function of S,T st f is one-to-one holds
for R being SubRelStr of S holds f | R is one-to-one
let f be Function of S,T; ::_thesis: ( f is one-to-one implies for R being SubRelStr of S holds f | R is one-to-one )
assume A1: f is one-to-one ; ::_thesis: for R being SubRelStr of S holds f | R is one-to-one
let R be SubRelStr of S; ::_thesis: f | R is one-to-one
 f | R = f | the carrier of R by Th6;
hence  f | R is one-to-one by A1, FUNCT_1:52; ::_thesis: verum
end;

registration
let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
let R be SubRelStr of S;
clusterf | R ->  monotone ;
coherence
 f | R is monotone
proof
let x, y be Element of R; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 ) )
A1: the carrier of R c= the carrier of S by YELLOW_0:def_13;
assume A2: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds
( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 )
then A3: [x,y] in the InternalRel of R by ORDERS_2:def_5;
then A4: x in the carrier of R by ZFMISC_1:87;
 y in the carrier of R by A3, ZFMISC_1:87;
then reconsider a = x, b = y as Element of S by A4, A1;
A5: a <= b by A2, YELLOW_0:59;
A6: f . b = (f | R) . y by A4, Th6;
 f . a = (f | R) . x by A4, Th6;
hence  for b1, b2 being Element of the carrier of T holds
( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 ) by A5, A6, WAYBEL_1:def_2; ::_thesis: verum
end;
end;

theorem Th8: :: WAYBEL10:8
for S, T being non empty RelStr
for R being non empty SubRelStr of S
for f being Function of S,T
for g being Function of T,S st f is V7() & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
proof
let S, T be non empty RelStr ; ::_thesis: for R being non empty SubRelStr of S
for f being Function of S,T
for g being Function of T,S st f is V7() & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
let R be non empty SubRelStr of S; ::_thesis: for f being Function of S,T
for g being Function of T,S st f is V7() & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
let f be Function of S,T; ::_thesis: for g being Function of T,S st f is V7() & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
let g be Function of T,S; ::_thesis: ( f is V7() & g = f " implies ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " ) )
assume that
A1: f is V7() and
A2: g = f " ; ::_thesis: ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
set h = g | (Image (f | R));
A3: dom f = the carrier of S by FUNCT_2:def_1;
A4: dom (g | (Image (f | R))) = the carrier of (Image (f | R)) by FUNCT_2:def_1;
A5: the carrier of R c= the carrier of S by YELLOW_0:def_13;
 rng (g | (Image (f | R))) c= the carrier of R
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (g | (Image (f | R))) or y in the carrier of R )
assume  y in rng (g | (Image (f | R))) ; ::_thesis: y in the carrier of R
then consider x being set  such that
A6: x in dom (g | (Image (f | R))) and
A7: y = (g | (Image (f | R))) . x by FUNCT_1:def_3;
reconsider x = x as Element of (Image (f | R)) by A6;
consider a being Element of R such that
A8: (f | R) . a = x by YELLOW_2:10;
A9: f . a = x by A8, Th6;
A10: a in the carrier of R ;
 y = g . x by A7, Th6;
hence  y in the carrier of R by A1, A2, A5, A3, A10, A9, FUNCT_1:32; ::_thesis: verum
end;
hence  g | (Image (f | R)) is Function of (Image (f | R)),R by A4, RELSET_1:4; ::_thesis: g | (Image (f | R)) = (f | R) "
A11: rng (f | R) = the carrier of (Image (f | R)) by YELLOW_0:def_15;
A12: f | R is V7() by A1, Th7;
A13: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Image_(f_|_R))_holds_
(g_|_(Image_(f_|_R)))_._x_=_((f_|_R)_")_._x
let x be set ; ::_thesis: ( x in the carrier of (Image (f | R)) implies (g | (Image (f | R))) . x = ((f | R) ") . x )
A14: dom (f | R) = the carrier of R by FUNCT_2:def_1;
assume A15: x in the carrier of (Image (f | R)) ; ::_thesis: (g | (Image (f | R))) . x = ((f | R) ") . x
then consider y being set  such that
A16: y in dom (f | R) and
A17: x = (f | R) . y by A11, FUNCT_1:def_3;
A18: y = ((f | R) ") . x by A12, A16, A17, FUNCT_1:32;
 x = f . y by A16, A17, Th6;
then  y = g . x by A1, A2, A5, A3, A16, A14, FUNCT_1:32;
hence  (g | (Image (f | R))) . x = ((f | R) ") . x by A15, A18, Th6; ::_thesis: verum
end;
 dom ((f | R) ") = rng (f | R) by A12, FUNCT_1:33;
hence  g | (Image (f | R)) = (f | R) " by A4, A11, A13, FUNCT_1:2; ::_thesis: verum
end;

begin

registration
let S be RelStr ;
let T be non empty reflexive RelStr ;
cluster MonMaps (S,T) ->  non empty ;
coherence
 not MonMaps (S,T) is empty
proof
set f = the monotone Function of S,T;
 the monotone Function of S,T in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8;
hence  not MonMaps (S,T) is empty by YELLOW_1:def_6; ::_thesis: verum
end;
end;

theorem Th9: :: WAYBEL10:9
for S being RelStr
for T being non empty reflexive RelStr
for x being set holds
( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T )
proof
let S be RelStr ; ::_thesis: for T being non empty reflexive RelStr
for x being set holds
( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T )
let T be non empty reflexive RelStr ; ::_thesis: for x being set holds
( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T )
let x be set ; ::_thesis: ( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T )
hereby  ::_thesis: ( x is monotone Function of S,T implies x is Element of (MonMaps (S,T)) )
assume  x is Element of (MonMaps (S,T)) ; ::_thesis: x is monotone Function of S,T
then reconsider f = x as Element of (MonMaps (S,T)) ;
 f is Element of (T |^ the carrier of S) by YELLOW_0:58;
then  f in the carrier of (T |^ the carrier of S) ;
then  f in Funcs ( the carrier of S, the carrier of T) by YELLOW_1:28;
then reconsider f = f as Function of S,T by FUNCT_2:66;
 f in the carrier of (MonMaps (S,T)) ;
hence  x is monotone Function of S,T by YELLOW_1:def_6; ::_thesis: verum
end;
assume  x is monotone Function of S,T ; ::_thesis: x is Element of (MonMaps (S,T))
then reconsider f = x as monotone Function of S,T ;
 f in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8;
hence  x is Element of (MonMaps (S,T)) by YELLOW_1:def_6; ::_thesis: verum
end;

definition
let L be non empty reflexive RelStr ;
func ClOpers L ->  non empty strict full SubRelStr of MonMaps (L,L) means :Def1: :: WAYBEL10:def 1
 for f being Function of L,L holds
( f is Element of it iff f is closure );
existence
 ex b1 being non empty strict full SubRelStr of MonMaps (L,L) st
for f being Function of L,L holds
( f is Element of b1 iff f is closure )
proof
defpred S1[ set ] means $1 is closure Function of L,L;
set h = the closure Function of L,L;
 the closure Function of L,L in Funcs ( the carrier of L, the carrier of L) by FUNCT_2:9;
then A1: the closure Function of L,L in the carrier of (MonMaps (L,L)) by YELLOW_1:def_6;
A2: S1[ the closure Function of L,L] ;
consider S being non empty strict full SubRelStr of MonMaps (L,L) such that
A3: for f being Element of (MonMaps (L,L)) holds
( f is Element of S iff S1[f] ) from WAYBEL10:sch_1(A2, A1);
take  S ; ::_thesis: for f being Function of L,L holds
( f is Element of S iff f is closure )
let f be Function of L,L; ::_thesis: ( f is Element of S iff f is closure )
hereby  ::_thesis: ( f is closure implies f is Element of S )
assume A4: f is Element of S ; ::_thesis: f is closure
then  f is Element of (MonMaps (L,L)) by YELLOW_0:58;
hence  f is closure by A3, A4; ::_thesis: verum
end;
assume A5: f is closure ; ::_thesis: f is Element of S
 f in Funcs ( the carrier of L, the carrier of L) by FUNCT_2:9;
then  f in the carrier of (MonMaps (L,L)) by A5, YELLOW_1:def_6;
hence  f is Element of S by A3, A5; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of MonMaps (L,L) st ( for f being Function of L,L holds
( f is Element of b1 iff f is closure ) ) & ( for f being Function of L,L holds
( f is Element of b2 iff f is closure ) ) holds
b1 = b2;
proof
let S1, S2 be non empty strict full SubRelStr of MonMaps (L,L); ::_thesis: ( ( for f being Function of L,L holds
( f is Element of S1 iff f is closure ) ) & ( for f being Function of L,L holds
( f is Element of S2 iff f is closure ) ) implies S1 = S2 )
assume that
A6: for f being Function of L,L holds
( f is Element of S1 iff f is closure ) and
A7: for f being Function of L,L holds
( f is Element of S2 iff f is closure ) ; ::_thesis: S1 = S2
 the carrier of S1 = the carrier of S2
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of S2 c= the carrier of S1
let x be set ; ::_thesis: ( x in the carrier of S1 implies x in the carrier of S2 )
assume  x in the carrier of S1 ; ::_thesis: x in the carrier of S2
then reconsider y = x as Element of S1 ;
 y is Element of (MonMaps (L,L)) by YELLOW_0:58;
then reconsider y = y as Function of L,L by Th9;
 y is closure by A6;
then  y is Element of S2 by A7;
hence  x in the carrier of S2 ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of S2 or x in the carrier of S1 )
assume  x in the carrier of S2 ; ::_thesis: x in the carrier of S1
then reconsider y = x as Element of S2 ;
 y is Element of (MonMaps (L,L)) by YELLOW_0:58;
then reconsider y = y as Function of L,L by Th9;
 y is closure by A7;
then  y is Element of S1 by A6;
hence  x in the carrier of S1 ; ::_thesis: verum
end;
hence  S1 = S2 by YELLOW_0:57; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines ClOpers WAYBEL10:def_1_:_
 for L being non empty reflexive RelStr
for b2 being non empty strict full SubRelStr of MonMaps (L,L) holds
( b2 = ClOpers L iff for f being Function of L,L holds
( f is Element of b2 iff f is closure ) );

theorem Th10: :: WAYBEL10:10
for L being non empty reflexive RelStr
for x being set holds
( x is Element of (ClOpers L) iff x is closure Function of L,L )
proof
let L be non empty reflexive RelStr ; ::_thesis: for x being set holds
( x is Element of (ClOpers L) iff x is closure Function of L,L )
let x be set ; ::_thesis: ( x is Element of (ClOpers L) iff x is closure Function of L,L )
 ( x is Element of (ClOpers L) implies x is Element of (MonMaps (L,L)) ) by YELLOW_0:58;
hence  ( x is Element of (ClOpers L) iff x is closure Function of L,L ) by Def1, Th9; ::_thesis: verum
end;

theorem Th11: :: WAYBEL10:11
for X being set
for L being non empty RelStr
for f, g being Function of X, the carrier of L
for x, y being Element of (L |^ X) st x = f & y = g holds
( x <= y iff f <= g )
proof
let X be set ; ::_thesis: for L being non empty RelStr
for f, g being Function of X, the carrier of L
for x, y being Element of (L |^ X) st x = f & y = g holds
( x <= y iff f <= g )
let L be non empty RelStr ; ::_thesis: for f, g being Function of X, the carrier of L
for x, y being Element of (L |^ X) st x = f & y = g holds
( x <= y iff f <= g )
let f, g be Function of X, the carrier of L; ::_thesis: for x, y being Element of (L |^ X) st x = f & y = g holds
( x <= y iff f <= g )
let x, y be Element of (L |^ X); ::_thesis: ( x = f & y = g implies ( x <= y iff f <= g ) )
assume that
A1: x = f and
A2: y = g ; ::_thesis: ( x <= y iff f <= g )
set J = X --> L;
A3: L |^ X = product (X --> L) by YELLOW_1:def_5;
A4: the carrier of (product (X --> L)) = product (Carrier (X --> L)) by YELLOW_1:def_4;
then A5: ( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) by A3, YELLOW_1:def_4;
hereby  ::_thesis: ( f <= g implies x <= y )
assume A6: x <= y ; ::_thesis: f <= g
thus  f <= g ::_thesis: verum
proof
let i be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not i in X or ex b1, b2 being Element of the carrier of L st
( b1 = f . i & b2 = g . i & b1 <= b2 ) )
assume A7: i in X ; ::_thesis: ex b1, b2 being Element of the carrier of L st
( b1 = f . i & b2 = g . i & b1 <= b2 )
then A8: (X --> L) . i = L by FUNCOP_1:7;
 ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f . i & yi = g . i & xi <= yi ) by A1, A2, A5, A6, A7;
hence  ex b1, b2 being Element of the carrier of L st
( b1 = f . i & b2 = g . i & b1 <= b2 ) by A8; ::_thesis: verum
end;
end;
assume A9: for j being set st j in X holds
ex a, b being Element of L st
( a = f . j & b = g . j & a <= b ) ; :: according to YELLOW_2:def_1 ::_thesis: x <= y
now__::_thesis:_ex_f9,_g9_being_Function_st_
(_f9_=_x_&_g9_=_y_&_(_for_i_being_set_st_i_in_X_holds_
ex_R_being_RelStr_ex_xi,_yi_being_Element_of_R_st_
(_R_=_(X_-->_L)_._i_&_xi_=_f9_._i_&_yi_=_g9_._i_&_xi_<=_yi_)_)_)
reconsider f9 = f, g9 = g as Function ;
take f9 = f9; ::_thesis: ex g9 being Function st
( f9 = x & g9 = y & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) ) )
take g9 = g9; ::_thesis: ( f9 = x & g9 = y & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) ) )
thus  ( f9 = x & g9 = y ) by A1, A2; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) )
assume A10: i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi )
then A11: (X --> L) . i = L by FUNCOP_1:7;
 ex a, b being Element of L st
( a = f . i & b = g . i & a <= b ) by A9, A10;
hence  ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) by A11; ::_thesis: verum
end;
hence  x <= y by A4, A3, YELLOW_1:def_4; ::_thesis: verum
end;

theorem Th12: :: WAYBEL10:12
for L being complete LATTICE
for c1, c2 being Function of L,L
for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds
( x <= y iff c1 <= c2 )
proof
let L be complete LATTICE; ::_thesis: for c1, c2 being Function of L,L
for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds
( x <= y iff c1 <= c2 )
let c1, c2 be Function of L,L; ::_thesis: for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds
( x <= y iff c1 <= c2 )
let x, y be Element of (ClOpers L); ::_thesis: ( x = c1 & y = c2 implies ( x <= y iff c1 <= c2 ) )
assume that
A1: x = c1 and
A2: y = c2 ; ::_thesis: ( x <= y iff c1 <= c2 )
reconsider x9 = x, y9 = y as Element of (MonMaps (L,L)) by YELLOW_0:58;
reconsider x99 = x9, y99 = y9 as Element of (L |^ the carrier of L) by YELLOW_0:58;
 ( x99 <= y99 iff x9 <= y9 ) by YELLOW_0:59, YELLOW_0:60;
hence  ( x <= y iff c1 <= c2 ) by A1, A2, Th11, YELLOW_0:59, YELLOW_0:60; ::_thesis: verum
end;

theorem Th13: :: WAYBEL10:13
for L being reflexive RelStr
for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds
S1 is SubRelStr of S2
proof
let L be reflexive RelStr ; ::_thesis: for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds
S1 is SubRelStr of S2
let S1, S2 be full SubRelStr of L; ::_thesis: ( the carrier of S1 c= the carrier of S2 implies S1 is SubRelStr of S2 )
assume A1: the carrier of S1 c= the carrier of S2 ; ::_thesis: S1 is SubRelStr of S2
hence  the carrier of S1 c= the carrier of S2 ; :: according to YELLOW_0:def_13 ::_thesis: the InternalRel of S1 c= the InternalRel of S2
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of S1 or [x,y] in the InternalRel of S2 )
assume A2: [x,y] in the InternalRel of S1 ; ::_thesis: [x,y] in the InternalRel of S2
then A3: x in the carrier of S1 by ZFMISC_1:87;
A4: y in the carrier of S1 by A2, ZFMISC_1:87;
reconsider x = x, y = y as Element of S1 by A2, ZFMISC_1:87;
 the carrier of S1 c= the carrier of L by YELLOW_0:def_13;
then reconsider a = x, b = y as Element of L by A3, A4;
reconsider x9 = x, y9 = y as Element of S2 by A1, A3, A4;
 x <= y by A2, ORDERS_2:def_5;
then  a <= b by YELLOW_0:59;
then  x9 <= y9 by A1, A3, YELLOW_0:60;
hence  [x,y] in the InternalRel of S2 by ORDERS_2:def_5; ::_thesis: verum
end;

theorem Th14: :: WAYBEL10:14
for L being complete LATTICE
for c1, c2 being closure Function of L,L holds
( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )
proof
let L be complete LATTICE; ::_thesis: for c1, c2 being closure Function of L,L holds
( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )
let c1, c2 be closure Function of L,L; ::_thesis: ( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )
hereby  ::_thesis: ( Image c2 is SubRelStr of Image c1 implies c1 <= c2 )
assume A1: c1 <= c2 ; ::_thesis: Image c2 is SubRelStr of Image c1
 the carrier of (Image c2) c= the carrier of (Image c1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Image c2) or x in the carrier of (Image c1) )
assume  x in the carrier of (Image c2) ; ::_thesis: x in the carrier of (Image c1)
then consider y being Element of L such that
A2: c2 . y = x by YELLOW_2:10;
A3: c2 . (c2 . y) = c2 . y by YELLOW_2:18;
A4: c1 . (c2 . y) <= c2 . (c2 . y) by A1, YELLOW_2:9;
 c2 . y <= c1 . (c2 . y) by Th5;
then  c1 . (c2 . y) = x by A2, A4, A3, ORDERS_2:2;
then  x in rng c1 by FUNCT_2:4;
hence  x in the carrier of (Image c1) by YELLOW_0:def_15; ::_thesis: verum
end;
hence  Image c2 is SubRelStr of Image c1 by Th13; ::_thesis: verum
end;
assume that
A5: the carrier of (Image c2) c= the carrier of (Image c1) and
 the InternalRel of (Image c2) c= the InternalRel of (Image c1) ; :: according to YELLOW_0:def_13 ::_thesis: c1 <= c2
now__::_thesis:_for_x_being_Element_of_L_holds_c1_._x_<=_c2_._x
let x be Element of L; ::_thesis: c1 . x <= c2 . x
 c2 . x in rng c2 by FUNCT_2:4;
then  c2 . x in the carrier of (Image c2) by YELLOW_0:def_15;
then  ex a being Element of L st c1 . a = c2 . x by A5, YELLOW_2:10;
then A6: c1 . (c2 . x) = c2 . x by YELLOW_2:18;
 x <= c2 . x by Th5;
hence  c1 . x <= c2 . x by A6, WAYBEL_1:def_2; ::_thesis: verum
end;
hence  c1 <= c2 by YELLOW_2:9; ::_thesis: verum
end;

begin

definition
let L be RelStr ;
func Sub L ->  non empty strict RelStr  means :Def2: :: WAYBEL10:def 2
( ( for x being set holds
( x is Element of it iff x is strict SubRelStr of L ) ) & ( for a, b being Element of it holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) );
existence
 ex b1 being non empty strict RelStr st
( ( for x being set holds
( x is Element of b1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b1 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) )
proof
set X =  {  RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L  }  ;
A1: the InternalRel of (subrelstr ({} L)) c= the InternalRel of L by YELLOW_0:def_13;
 the carrier of (subrelstr ({} L)) = {} L by YELLOW_0:def_15;
then  subrelstr ({} L) in  {  RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L  }  by A1;
then reconsider X =  {  RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L  }  as non empty set ;
defpred S1[ set , set ] means  ex R being RelStr st
( $2 = R & $1 is SubRelStr of R );
consider S being non empty strict RelStr  such that
A2: the carrier of S = X and
A3: for a, b being Element of S holds
( a <= b iff S1[a,b] ) from YELLOW_0:sch_1();
take  S ; ::_thesis: ( ( for x being set holds
( x is Element of S iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) )
hereby  ::_thesis: for a, b being Element of S holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) )
let x be set ; ::_thesis: ( ( x is Element of S implies x is strict SubRelStr of L ) & ( x is strict SubRelStr of L implies x is Element of S ) )
hereby  ::_thesis: ( x is strict SubRelStr of L implies x is Element of S )
assume  x is Element of S ; ::_thesis: x is strict SubRelStr of L
then  x in X by A2;
then  ex A being Subset of L ex B being Relation of A,A st
( x = RelStr(# A,B #) & B c= the InternalRel of L ) ;
hence  x is strict SubRelStr of L by YELLOW_0:def_13; ::_thesis: verum
end;
assume  x is strict SubRelStr of L ; ::_thesis: x is Element of S
then reconsider R = x as strict SubRelStr of L ;
A4: the InternalRel of R c= the InternalRel of L by YELLOW_0:def_13;
 the carrier of R c= the carrier of L by YELLOW_0:def_13;
then  R in X by A4;
hence  x is Element of S by A2; ::_thesis: verum
end;
thus  for a, b being Element of S holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) by A3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict RelStr st ( for x being set holds
( x is Element of b1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b1 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) & ( for x being set holds
( x is Element of b2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b2 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) holds
b1 = b2;
proof
defpred S1[ set , set ] means  ex R being RelStr st
( $2 = R & $1 is SubRelStr of R );
defpred S2[ set ] means $1 is strict SubRelStr of L;
let S1, S2 be non empty strict RelStr ; ::_thesis: ( ( for x being set holds
( x is Element of S1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S1 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) & ( for x being set holds
( x is Element of S2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S2 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) implies S1 = S2 )
assume that
A5: for x being set holds
( x is Element of S1 iff S2[x] ) and
A6: for a, b being Element of S1 holds
( a <= b iff S1[a,b] ) and
A7: for x being set holds
( x is Element of S2 iff S2[x] ) and
A8: for a, b being Element of S2 holds
( a <= b iff S1[a,b] ) ; ::_thesis: S1 = S2
 RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch_2(A5, A7, A6, A8);
hence  S1 = S2 ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Sub WAYBEL10:def_2_:_
 for L being RelStr
for b2 being non empty strict RelStr holds
( b2 = Sub L iff ( ( for x being set holds
( x is Element of b2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b2 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) ) );

theorem Th15: :: WAYBEL10:15
for L, R being RelStr
for x, y being Element of (Sub L) st y = R holds
( x <= y iff x is SubRelStr of R )
proof
let L, R be RelStr ; ::_thesis: for x, y being Element of (Sub L) st y = R holds
( x <= y iff x is SubRelStr of R )
let x, y be Element of (Sub L); ::_thesis: ( y = R implies ( x <= y iff x is SubRelStr of R ) )
 ( x <= y iff ex R being RelStr st
( y = R & x is SubRelStr of R ) ) by Def2;
hence  ( y = R implies ( x <= y iff x is SubRelStr of R ) ) ; ::_thesis: verum
end;

registration
let L be RelStr ;
cluster Sub L ->  non empty strict reflexive transitive antisymmetric ;
coherence
 ( Sub L is reflexive & Sub L is antisymmetric & Sub L is transitive )
proof
set R = Sub L;
thus  Sub L is reflexive ::_thesis: ( Sub L is antisymmetric & Sub L is transitive )
proof
let x be Element of (Sub L); :: according to YELLOW_0:def_1 ::_thesis: x <= x
reconsider A = x as strict SubRelStr of L by Def2;
 A is SubRelStr of A by YELLOW_0:def_13;
hence  x <= x by Th15; ::_thesis: verum
end;
thus  Sub L is antisymmetric ::_thesis: Sub L is transitive
proof
let x, y be Element of (Sub L); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
reconsider A = x, B = y as strict SubRelStr of L by Def2;
assume that
A1: x <= y and
A2: y <= x ; ::_thesis: x = y
A3: B is SubRelStr of A by A2, Th15;
then A4: the carrier of B c= the carrier of A by YELLOW_0:def_13;
A5: A is SubRelStr of B by A1, Th15;
then  the carrier of A c= the carrier of B by YELLOW_0:def_13;
then A6: the carrier of A = the carrier of B by A4, XBOOLE_0:def_10;
A7: the InternalRel of B c= the InternalRel of A by A3, YELLOW_0:def_13;
 the InternalRel of A c= the InternalRel of B by A5, YELLOW_0:def_13;
hence  x = y by A7, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  Sub L is transitive ::_thesis: verum
proof
let x, y, z be Element of (Sub L); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
reconsider A = x, B = y, C = z as strict SubRelStr of L by Def2;
assume that
A8: x <= y and
A9: y <= z ; ::_thesis: x <= z
A10: B is SubRelStr of C by A9, Th15;
then A11: the carrier of B c= the carrier of C by YELLOW_0:def_13;
A12: the InternalRel of B c= the InternalRel of C by A10, YELLOW_0:def_13;
A13: A is SubRelStr of B by A8, Th15;
then  the InternalRel of A c= the InternalRel of B by YELLOW_0:def_13;
then A14: the InternalRel of A c= the InternalRel of C by A12, XBOOLE_1:1;
 the carrier of A c= the carrier of B by A13, YELLOW_0:def_13;
then  the carrier of A c= the carrier of C by A11, XBOOLE_1:1;
then  A is SubRelStr of C by A14, YELLOW_0:def_13;
hence  x <= z by Th15; ::_thesis: verum
end;
end;
end;

registration
let L be RelStr ;
cluster Sub L ->  non empty strict complete ;
coherence
 Sub L is complete
proof
now__::_thesis:_for_X_being_Subset_of_(Sub_L)_holds_ex_sup_of_X,_Sub_L
let X be Subset of (Sub L); ::_thesis: ex_sup_of X, Sub L
now__::_thesis:_ex_a_being_Element_of_(Sub_L)_st_
(_X_is_<=_than_a_&_(_for_b_being_Element_of_(Sub_L)_st_X_is_<=_than_b_holds_
a_<=_b_)_)
defpred S1[ set ] means  ex R being RelStr st
( R in X & L in the InternalRel of R );
defpred S2[ set ] means  ex R being RelStr st
( R in X & L in the carrier of R );
consider Y being set  such that
A1: for x being set holds
( x in Y iff ( x in the carrier of L & S2[x] ) ) from XBOOLE_0:sch_1();
consider S being set  such that
A2: for x being set holds
( x in S iff ( x in the InternalRel of L & S1[x] ) ) from XBOOLE_0:sch_1();
A3: S c= [:Y,Y:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in [:Y,Y:] )
assume  x in S ; ::_thesis: x in [:Y,Y:]
then consider R being RelStr  such that
A4: R in X and
A5: x in the InternalRel of R by A2;
 the carrier of R c= Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in Y )
 R is SubRelStr of L by A4, Def2;
then A6: the carrier of R c= the carrier of L by YELLOW_0:def_13;
assume  x in the carrier of R ; ::_thesis: x in Y
hence  x in Y by A1, A4, A6; ::_thesis: verum
end;
then A7: [: the carrier of R, the carrier of R:] c= [:Y,Y:] by ZFMISC_1:96;
 x in [: the carrier of R, the carrier of R:] by A5;
hence  x in [:Y,Y:] by A7; ::_thesis: verum
end;
A8: S c= the InternalRel of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in the InternalRel of L )
thus  ( not x in S or x in the InternalRel of L ) by A2; ::_thesis: verum
end;
reconsider S = S as Relation of Y by A3;
 Y c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in the carrier of L )
thus  ( not x in Y or x in the carrier of L ) by A1; ::_thesis: verum
end;
then reconsider A = RelStr(# Y,S #) as SubRelStr of L by A8, YELLOW_0:def_13;
reconsider a = A as Element of (Sub L) by Def2;
take a = a; ::_thesis: ( X is_<=_than a & ( for b being Element of (Sub L) st X is_<=_than b holds
a <= b ) )
thus  X is_<=_than a ::_thesis: for b being Element of (Sub L) st X is_<=_than b holds
a <= b
proof
let b be Element of (Sub L); :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= a )
reconsider R = b as strict SubRelStr of L by Def2;
assume A9: b in X ; ::_thesis: b <= a
A10: the InternalRel of R c= S
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of R or [x,y] in S )
A11: the InternalRel of R c= the InternalRel of L by YELLOW_0:def_13;
assume  [x,y] in the InternalRel of R ; ::_thesis: [x,y] in S
hence  [x,y] in S by A2, A9, A11; ::_thesis: verum
end;
 the carrier of R c= Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in Y )
A12: the carrier of R c= the carrier of L by YELLOW_0:def_13;
assume  x in the carrier of R ; ::_thesis: x in Y
hence  x in Y by A1, A9, A12; ::_thesis: verum
end;
then  R is SubRelStr of A by A10, YELLOW_0:def_13;
hence  b <= a by Th15; ::_thesis: verum
end;
let b be Element of (Sub L); ::_thesis: ( X is_<=_than b implies a <= b )
reconsider B = b as strict SubRelStr of L by Def2;
assume A13: X is_<=_than b ; ::_thesis: a <= b
A14: S c= the InternalRel of B
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in S or [x,y] in the InternalRel of B )
assume  [x,y] in S ; ::_thesis: [x,y] in the InternalRel of B
then consider R being RelStr  such that
A15: R in X and
A16: [x,y] in the InternalRel of R by A2;
reconsider c = R as Element of (Sub L) by A15;
 c <= b by A13, A15, LATTICE3:def_9;
then  R is SubRelStr of B by Th15;
then  the InternalRel of R c= the InternalRel of B by YELLOW_0:def_13;
hence  [x,y] in the InternalRel of B by A16; ::_thesis: verum
end;
 Y c= the carrier of B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in the carrier of B )
assume  x in Y ; ::_thesis: x in the carrier of B
then consider R being RelStr  such that
A17: R in X and
A18: x in the carrier of R by A1;
reconsider c = R as Element of (Sub L) by A17;
 c <= b by A13, A17, LATTICE3:def_9;
then  R is SubRelStr of B by Th15;
then  the carrier of R c= the carrier of B by YELLOW_0:def_13;
hence  x in the carrier of B by A18; ::_thesis: verum
end;
then  a is SubRelStr of B by A14, YELLOW_0:def_13;
hence  a <= b by Th15; ::_thesis: verum
end;
hence  ex_sup_of X, Sub L by YELLOW_0:15; ::_thesis: verum
end;
hence  Sub L is complete by YELLOW_0:53; ::_thesis: verum
end;
end;

registration
let L be complete LATTICE;
cluster infs-inheriting  ->  non empty for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is infs-inheriting holds
not b1 is empty
proof
let S be SubRelStr of L; ::_thesis: ( S is infs-inheriting implies not S is empty )
assume A1: S is infs-inheriting ; ::_thesis: not S is empty
 ex_inf_of {} S,L by YELLOW_0:17;
hence  not S is empty by A1, YELLOW_0:def_18; ::_thesis: verum
end;
cluster sups-inheriting  ->  non empty for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is sups-inheriting holds
not b1 is empty
proof
let S be SubRelStr of L; ::_thesis: ( S is sups-inheriting implies not S is empty )
assume A2: S is sups-inheriting ; ::_thesis: not S is empty
 ex_sup_of {} S,L by YELLOW_0:17;
hence  not S is empty by A2, YELLOW_0:def_19; ::_thesis: verum
end;
end;

definition
let L be RelStr ;
mode System of L is full SubRelStr of L;
end;

notation
let L be non empty RelStr ;
let S be System of L;
synonym  closure S for  infs-inheriting ;
end;

registration
let L be non empty RelStr ;
cluster subrelstr ([#] L) ->  infs-inheriting sups-inheriting ;
coherence
 ( subrelstr ([#] L) is closure & subrelstr ([#] L) is sups-inheriting )
proof
set SL = subrelstr ([#] L);
A1: the carrier of (subrelstr ([#] L)) = the carrier of L by YELLOW_0:def_15;
thus  subrelstr ([#] L) is infs-inheriting ::_thesis: subrelstr ([#] L) is sups-inheriting
proof
let X be Subset of (subrelstr ([#] L)); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr ([#] L)) )
thus  ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr ([#] L)) ) by A1; ::_thesis: verum
end;
let X be Subset of (subrelstr ([#] L)); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr ([#] L)) )
thus  ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr ([#] L)) ) by A1; ::_thesis: verum
end;
end;

definition
let L be non empty RelStr ;
func ClosureSystems L ->  non empty strict full SubRelStr of Sub L means :Def3: :: WAYBEL10:def 3
 for R being strict SubRelStr of L holds
( R is Element of it iff ( R is infs-inheriting & R is full ) );
existence
 ex b1 being non empty strict full SubRelStr of Sub L st
for R being strict SubRelStr of L holds
( R is Element of b1 iff ( R is infs-inheriting & R is full ) )
proof
defpred S1[ set ] means $1 is full infs-inheriting SubRelStr of L;
set SL = subrelstr ([#] L);
 subrelstr ([#] L) is Element of (Sub L) by Def2;
then A1: subrelstr ([#] L) in the carrier of (Sub L) ;
A2: S1[ subrelstr ([#] L)] ;
consider S being non empty strict full SubRelStr of Sub L such that
A3: for x being Element of (Sub L) holds
( x is Element of S iff S1[x] ) from WAYBEL10:sch_1(A2, A1);
take  S ; ::_thesis: for R being strict SubRelStr of L holds
( R is Element of S iff ( R is infs-inheriting & R is full ) )
let R be strict SubRelStr of L; ::_thesis: ( R is Element of S iff ( R is infs-inheriting & R is full ) )
 R is Element of (Sub L) by Def2;
hence  ( R is Element of S iff ( R is infs-inheriting & R is full ) ) by A3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of Sub L st ( for R being strict SubRelStr of L holds
( R is Element of b1 iff ( R is infs-inheriting & R is full ) ) ) & ( for R being strict SubRelStr of L holds
( R is Element of b2 iff ( R is infs-inheriting & R is full ) ) ) holds
b1 = b2;
proof
defpred S1[ set ] means $1 is strict full infs-inheriting SubRelStr of L;
let S1, S2 be non empty strict full SubRelStr of Sub L; ::_thesis: ( ( for R being strict SubRelStr of L holds
( R is Element of S1 iff ( R is infs-inheriting & R is full ) ) ) & ( for R being strict SubRelStr of L holds
( R is Element of S2 iff ( R is infs-inheriting & R is full ) ) ) implies S1 = S2 )
assume that
A4: for R being strict SubRelStr of L holds
( R is Element of S1 iff ( R is infs-inheriting & R is full ) ) and
A5: for R being strict SubRelStr of L holds
( R is Element of S2 iff ( R is infs-inheriting & R is full ) ) ; ::_thesis: S1 = S2
A6: now__::_thesis:_for_x_being_set_holds_
(_x_is_Element_of_S2_iff_S1[x]_)
let x be set ; ::_thesis: ( x is Element of S2 iff S1[x] )
 ( x is Element of S2 implies x is Element of (Sub L) ) by YELLOW_0:58;
then  ( x is Element of S2 implies x is strict SubRelStr of L ) by Def2;
hence  ( x is Element of S2 iff S1[x] ) by A5; ::_thesis: verum
end;
A7: now__::_thesis:_for_x_being_set_holds_
(_x_is_Element_of_S1_iff_S1[x]_)
let x be set ; ::_thesis: ( x is Element of S1 iff S1[x] )
 ( x is Element of S1 implies x is Element of (Sub L) ) by YELLOW_0:58;
then  ( x is Element of S1 implies x is strict SubRelStr of L ) by Def2;
hence  ( x is Element of S1 iff S1[x] ) by A4; ::_thesis: verum
end;
 RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch_3(A7, A6);
hence  S1 = S2 ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines ClosureSystems WAYBEL10:def_3_:_
 for L being non empty RelStr
for b2 being non empty strict full SubRelStr of Sub L holds
( b2 = ClosureSystems L iff for R being strict SubRelStr of L holds
( R is Element of b2 iff ( R is infs-inheriting & R is full ) ) );

theorem Th16: :: WAYBEL10:16
for L being non empty RelStr
for x being set holds
( x is Element of (ClosureSystems L) iff x is strict closure System of L )
proof
let L be non empty RelStr ; ::_thesis: for x being set holds
( x is Element of (ClosureSystems L) iff x is strict closure System of L )
let x be set ; ::_thesis: ( x is Element of (ClosureSystems L) iff x is strict closure System of L )
 ( x is Element of (ClosureSystems L) implies x is Element of (Sub L) ) by YELLOW_0:58;
then  ( x is Element of (ClosureSystems L) implies x is strict SubRelStr of L ) by Def2;
hence  ( x is Element of (ClosureSystems L) iff x is strict closure System of L ) by Def3; ::_thesis: verum
end;

theorem Th17: :: WAYBEL10:17
for L being non empty RelStr
for R being RelStr
for x, y being Element of (ClosureSystems L) st y = R holds
( x <= y iff x is SubRelStr of R )
proof
let L be non empty RelStr ; ::_thesis: for R being RelStr
for x, y being Element of (ClosureSystems L) st y = R holds
( x <= y iff x is SubRelStr of R )
let R be RelStr ; ::_thesis: for x, y being Element of (ClosureSystems L) st y = R holds
( x <= y iff x is SubRelStr of R )
let x, y be Element of (ClosureSystems L); ::_thesis: ( y = R implies ( x <= y iff x is SubRelStr of R ) )
reconsider a = x, b = y as Element of (Sub L) by YELLOW_0:58;
 ( x <= y iff a <= b ) by YELLOW_0:59, YELLOW_0:60;
hence  ( y = R implies ( x <= y iff x is SubRelStr of R ) ) by Th15; ::_thesis: verum
end;

begin

registration
let L be non empty Poset;
let h be closure Function of L,L;
cluster Image h ->  infs-inheriting ;
coherence
 Image h is closure by WAYBEL_1:53;
end;

definition
let L be non empty Poset;
func ClImageMap L ->  Function of (ClOpers L),((ClosureSystems L) opp) means :Def4: :: WAYBEL10:def 4
 for c being closure Function of L,L holds it . c = Image c;
existence
 ex b1 being Function of (ClOpers L),((ClosureSystems L) opp) st
for c being closure Function of L,L holds b1 . c = Image c
proof
defpred S1[ set , set ] means  ex c being closure Function of L,L st
( c = $1 & $2 = Image c );
A1: now__::_thesis:_for_x_being_Element_of_(ClOpers_L)_ex_b_being_Element_of_the_carrier_of_((ClosureSystems_L)_~)_st_S1[x,b]
let x be Element of (ClOpers L); ::_thesis: ex b being Element of the carrier of ((ClosureSystems L) ~) st S1[x,b]
reconsider c = x as closure Function of L,L by Th10;
reconsider a = Image c as Element of (ClosureSystems L) by Th16;
take b = a ~ ; ::_thesis: S1[x,b]
thus  S1[x,b] ; ::_thesis: verum
end;
consider f being Function of (ClOpers L),((ClosureSystems L) opp) such that
A2: for x being Element of (ClOpers L) holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for c being closure Function of L,L holds f . c = Image c
let c be closure Function of L,L; ::_thesis: f . c = Image c
 c is Element of (ClOpers L) by Th10;
then  ex c1 being closure Function of L,L st
( c1 = c & f . c = Image c1 ) by A2;
hence  f . c = Image c ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Function of (ClOpers L),((ClosureSystems L) opp) st ( for c being closure Function of L,L holds b1 . c = Image c ) & ( for c being closure Function of L,L holds b2 . c = Image c ) holds
b1 = b2;
proof
let f1, f2 be Function of (ClOpers L),((ClosureSystems L) opp); ::_thesis: ( ( for c being closure Function of L,L holds f1 . c = Image c ) & ( for c being closure Function of L,L holds f2 . c = Image c ) implies f1 = f2 )
assume that
A3: for c being closure Function of L,L holds f1 . c = Image c and
A4: for c being closure Function of L,L holds f2 . c = Image c ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_(ClOpers_L)_holds_f1_._x_=_f2_._x
let x be Element of (ClOpers L); ::_thesis: f1 . x = f2 . x
reconsider c = x as closure Function of L,L by Th10;
thus f1 . x = Image c by A3
.= f2 . x by A4 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines ClImageMap WAYBEL10:def_4_:_
 for L being non empty Poset
for b2 being Function of (ClOpers L),((ClosureSystems L) opp) holds
( b2 = ClImageMap L iff for c being closure Function of L,L holds b2 . c = Image c );

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
func closure_op S ->  Function of L,L means :Def5: :: WAYBEL10:def 5
 for x being Element of L holds it . x = "/\" (((uparrow x) /\ the carrier of S),L);
existence
 ex b1 being Function of L,L st
for x being Element of L holds b1 . x = "/\" (((uparrow x) /\ the carrier of S),L)
proof
deffunc H1( Element of L) ->  Element of the carrier of L = "/\" (((uparrow $1) /\ the carrier of S),L);
thus  ex f being Function of L,L st
for x being Element of L holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of L,L st ( for x being Element of L holds b1 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) & ( for x being Element of L holds b2 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) holds
b1 = b2
proof
let f1, f2 be Function of L,L; ::_thesis: ( ( for x being Element of L holds f1 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) & ( for x being Element of L holds f2 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) implies f1 = f2 )
assume that
A1: for x being Element of L holds f1 . x = "/\" (((uparrow x) /\ the carrier of S),L) and
A2: for x being Element of L holds f2 . x = "/\" (((uparrow x) /\ the carrier of S),L) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_L_holds_f1_._x_=_f2_._x
let x be Element of L; ::_thesis: f1 . x = f2 . x
thus f1 . x = "/\" (((uparrow x) /\ the carrier of S),L) by A1
.= f2 . x by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines closure_op WAYBEL10:def_5_:_
 for L being non empty RelStr
for S being SubRelStr of L
for b3 being Function of L,L holds
( b3 = closure_op S iff for x being Element of L holds b3 . x = "/\" (((uparrow x) /\ the carrier of S),L) );

registration
let L be complete LATTICE;
let S be closure System of L;
cluster closure_op S ->  closure ;
coherence
 closure_op S is closure
proof
set c = closure_op S;
reconsider cc = (closure_op S) * (closure_op S) as Function of L,L ;
A1: now__::_thesis:_for_x_being_Element_of_L_holds_
(_(id_L)_._x_=_x_&_(id_L)_._x_<=_(closure_op_S)_._x_)
let x be Element of L; ::_thesis: ( (id L) . x = x & (id L) . x <= (closure_op S) . x )
thus A2: (id L) . x = x by FUNCT_1:18; ::_thesis: (id L) . x <= (closure_op S) . x
 (uparrow x) /\ the carrier of S c= uparrow x by XBOOLE_1:17;
then A3: x is_<=_than (uparrow x) /\ the carrier of S by YELLOW_2:2;
 (closure_op S) . x = "/\" (((uparrow x) /\ the carrier of S),L) by Def5;
hence  (id L) . x <= (closure_op S) . x by A2, A3, YELLOW_0:33; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_L_holds_cc_._x_=_(closure_op_S)_._x
let x be Element of L; ::_thesis: cc . x = (closure_op S) . x
set y = (closure_op S) . x;
set X = (uparrow x) /\ the carrier of S;
reconsider X = (uparrow x) /\ the carrier of S as Subset of S by XBOOLE_1:17;
A4: (closure_op S) . ((closure_op S) . x) = "/\" (((uparrow ((closure_op S) . x)) /\ the carrier of S),L) by Def5;
 (closure_op S) . x <= (closure_op S) . x ;
then A5: (closure_op S) . x in uparrow ((closure_op S) . x) by WAYBEL_0:18;
 ex_inf_of X,L by YELLOW_0:17;
then A6: "/\" (X,L) in the carrier of S by YELLOW_0:def_18;
 (closure_op S) . x = "/\" (((uparrow x) /\ the carrier of S),L) by Def5;
then  (closure_op S) . x in (uparrow ((closure_op S) . x)) /\ the carrier of S by A6, A5, XBOOLE_0:def_4;
then A7: (closure_op S) . ((closure_op S) . x) <= (closure_op S) . x by A4, YELLOW_2:22;
A8: (closure_op S) . ((closure_op S) . x) >= (id L) . ((closure_op S) . x) by A1;
A9: (id L) . ((closure_op S) . x) = (closure_op S) . x by A1;
thus cc . x = (closure_op S) . ((closure_op S) . x) by FUNCT_2:15
.= (closure_op S) . x by A7, A8, A9, ORDERS_2:2 ; ::_thesis: verum
end;
hence  (closure_op S) * (closure_op S) = closure_op S by FUNCT_2:63; :: according to QUANTAL1:def_9,WAYBEL_1:def_13,WAYBEL_1:def_14 ::_thesis: ( closure_op S is monotone & id L <= closure_op S )
hereby  :: according to WAYBEL_1:def_2 ::_thesis: id L <= closure_op S
let x, y be Element of L; ::_thesis: ( x <= y implies (closure_op S) . x <= (closure_op S) . y )
A10: ex_inf_of (uparrow x) /\ the carrier of S,L by YELLOW_0:17;
A11: ex_inf_of (uparrow y) /\ the carrier of S,L by YELLOW_0:17;
assume  x <= y ; ::_thesis: (closure_op S) . x <= (closure_op S) . y
then A12: (uparrow y) /\ the carrier of S c= (uparrow x) /\ the carrier of S by WAYBEL_0:22, XBOOLE_1:26;
A13: (closure_op S) . y = "/\" (((uparrow y) /\ the carrier of S),L) by Def5;
 (closure_op S) . x = "/\" (((uparrow x) /\ the carrier of S),L) by Def5;
hence  (closure_op S) . x <= (closure_op S) . y by A12, A10, A11, A13, YELLOW_0:35; ::_thesis: verum
end;
let x be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not x in the carrier of L or ex b1, b2 being Element of the carrier of L st
( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 ) )
assume  x in the carrier of L ; ::_thesis: ex b1, b2 being Element of the carrier of L st
( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 )
then reconsider x = x as Element of L ;
 (id L) . x <= (closure_op S) . x by A1;
hence  ex b1, b2 being Element of the carrier of L st
( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 ) ; ::_thesis: verum
end;
end;

theorem Th18: :: WAYBEL10:18
for L being complete LATTICE
for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)
proof
let L be complete LATTICE; ::_thesis: for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)
let S be non empty full infs-inheriting SubRelStr of L; ::_thesis: Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)
 the carrier of (Image (closure_op S)) = the carrier of S
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of S c= the carrier of (Image (closure_op S))
let x be set ; ::_thesis: ( x in the carrier of (Image (closure_op S)) implies x in the carrier of S )
assume  x in the carrier of (Image (closure_op S)) ; ::_thesis: x in the carrier of S
then reconsider a = x as Element of (Image (closure_op S)) ;
consider b being Element of L such that
A1: a = (closure_op S) . b by YELLOW_2:10;
set X = (uparrow b) /\ the carrier of S;
reconsider X = (uparrow b) /\ the carrier of S as Subset of S by XBOOLE_1:17;
A2: ex_inf_of X,L by YELLOW_0:17;
 a = "/\" (X,L) by A1, Def5;
hence  x in the carrier of S by A2, YELLOW_0:def_18; ::_thesis: verum
end;
set c = closure_op S;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of S or x in the carrier of (Image (closure_op S)) )
assume  x in the carrier of S ; ::_thesis: x in the carrier of (Image (closure_op S))
then reconsider a = x as Element of S ;
reconsider a = a as Element of L by YELLOW_0:58;
set X = (uparrow a) /\ the carrier of S;
A3: (id L) . a = a by FUNCT_1:18;
 a <= a ;
then  a in uparrow a by WAYBEL_0:18;
then A4: a in (uparrow a) /\ the carrier of S by XBOOLE_0:def_4;
 (closure_op S) . a = "/\" (((uparrow a) /\ the carrier of S),L) by Def5;
then A5: (closure_op S) . a <= a by A4, YELLOW_2:22;
 id L <= closure_op S by WAYBEL_1:def_14;
then  a <= (closure_op S) . a by A3, YELLOW_2:9;
then A6: a = (closure_op S) . a by A5, ORDERS_2:2;
 dom (closure_op S) = the carrier of L by FUNCT_2:def_1;
then  a in rng (closure_op S) by A6, FUNCT_1:def_3;
hence  x in the carrier of (Image (closure_op S)) by YELLOW_0:def_15; ::_thesis: verum
end;
hence  Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_0:57; ::_thesis: verum
end;

theorem Th19: :: WAYBEL10:19
for L being complete LATTICE
for c being closure Function of L,L holds closure_op (Image c) = c
proof
let L be complete LATTICE; ::_thesis: for c being closure Function of L,L holds closure_op (Image c) = c
let c be closure Function of L,L; ::_thesis: closure_op (Image c) = c
now__::_thesis:_for_x_being_Element_of_L_holds_(closure_op_(Image_c))_._x_=_c_._x
let x be Element of L; ::_thesis: (closure_op (Image c)) . x = c . x
A1: id L <= c by WAYBEL_1:def_14;
 x = (id L) . x by FUNCT_1:18;
then  x <= c . x by A1, YELLOW_2:9;
then A2: c . x in uparrow x by WAYBEL_0:18;
 dom c = the carrier of L by FUNCT_2:def_1;
then  c . x in rng c by FUNCT_1:def_3;
then  c . x in (uparrow x) /\ (rng c) by A2, XBOOLE_0:def_4;
then A3: c . x >= "/\" (((uparrow x) /\ (rng c)),L) by YELLOW_2:22;
 c . x is_<=_than (uparrow x) /\ (rng c)
proof
let z be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not z in (uparrow x) /\ (rng c) or c . x <= z )
assume A4: z in (uparrow x) /\ (rng c) ; ::_thesis: c . x <= z
then  z in rng c by XBOOLE_0:def_4;
then consider a being set  such that
A5: a in dom c and
A6: z = c . a by FUNCT_1:def_3;
reconsider a = a as Element of L by A5;
 z in uparrow x by A4, XBOOLE_0:def_4;
then  x <= c . a by A6, WAYBEL_0:18;
then  c . x <= c . (c . a) by WAYBEL_1:def_2;
hence  c . x <= z by A6, YELLOW_2:18; ::_thesis: verum
end;
then A7: c . x <= "/\" (((uparrow x) /\ (rng c)),L) by YELLOW_0:33;
 rng c = the carrier of (Image c) by YELLOW_0:def_15;
hence (closure_op (Image c)) . x = "/\" (((uparrow x) /\ (rng c)),L) by Def5
.= c . x by A3, A7, ORDERS_2:2 ;
::_thesis: verum
end;
hence  closure_op (Image c) = c by FUNCT_2:63; ::_thesis: verum
end;

registration
let L be complete LATTICE;
cluster ClImageMap L -> V7() ;
coherence
 ClImageMap L is one-to-one
proof
let x, y be Element of (ClOpers L); :: according to WAYBEL_1:def_1 ::_thesis: ( not (ClImageMap L) . x = (ClImageMap L) . y or x = y )
reconsider a = x, b = y as closure Function of L,L by Th10;
set f = ClImageMap L;
assume  (ClImageMap L) . x = (ClImageMap L) . y ; ::_thesis: x = y
then  Image a = (ClImageMap L) . y by Def4
.= Image b by Def4 ;
hence x = closure_op (Image b) by Th19
.= y by Th19 ;
::_thesis: verum
end;
end;

theorem Th20: :: WAYBEL10:20
for L being complete LATTICE holds (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L)
proof
let L be complete LATTICE; ::_thesis: (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L)
set f = ClImageMap L;
A1: rng ((ClImageMap L) ") = dom (ClImageMap L) by FUNCT_1:33;
A2: dom (ClImageMap L) = the carrier of (ClOpers L) by FUNCT_2:def_1;
 the carrier of ((ClosureSystems L) opp) c= rng (ClImageMap L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((ClosureSystems L) opp) or x in rng (ClImageMap L) )
assume  x in the carrier of ((ClosureSystems L) opp) ; ::_thesis: x in rng (ClImageMap L)
then reconsider x = x as Element of ((ClosureSystems L) opp) ;
reconsider x = x as strict full infs-inheriting SubRelStr of L by Th16;
A3: closure_op x is Element of (ClOpers L) by Th10;
(ClImageMap L) . (closure_op x) = Image (closure_op x) by Def4
.= x by Th18 ;
hence  x in rng (ClImageMap L) by A2, A3, FUNCT_1:def_3; ::_thesis: verum
end;
then A4: the carrier of ((ClosureSystems L) opp) = rng (ClImageMap L) by XBOOLE_0:def_10;
 dom ((ClImageMap L) ") = rng (ClImageMap L) by FUNCT_1:33;
hence  (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L) by A1, A4, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;

theorem Th21: :: WAYBEL10:21
for L being complete LATTICE
for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S
proof
let L be complete LATTICE; ::_thesis: for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S
let S be strict full infs-inheriting SubRelStr of L; ::_thesis: ((ClImageMap L) ") . S = closure_op S
A1: closure_op S is Element of (ClOpers L) by Th10;
(ClImageMap L) . (closure_op S) = Image (closure_op S) by Def4
.= S by Th18 ;
hence  ((ClImageMap L) ") . S = closure_op S by A1, FUNCT_2:26; ::_thesis: verum
end;

registration
let L be complete LATTICE;
cluster ClImageMap L ->  isomorphic ;
correctness
coherence
ClImageMap L is isomorphic ;
proof
set f = ClImageMap L;
set S = ClOpers L;
set T = (ClosureSystems L) opp ;
reconsider g = (ClImageMap L) " as Function of ((ClosureSystems L) opp),(ClOpers L) by Th20;
percases ( ( not ClOpers L is empty & not (ClosureSystems L) opp is empty ) or ClOpers L is empty or (ClosureSystems L) opp is empty ) ;
:: according to WAYBEL_0:def_38
case ( not ClOpers L is empty & not (ClosureSystems L) opp is empty ) ; ::_thesis: ( ClImageMap L is one-to-one & ClImageMap L is monotone & ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st
( b1 = (ClImageMap L) " & b1 is monotone ) )
thus  ClImageMap L is V7() ; ::_thesis: ( ClImageMap L is monotone & ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st
( b1 = (ClImageMap L) " & b1 is monotone ) )
thus  ClImageMap L is monotone ::_thesis: ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st
( b1 = (ClImageMap L) " & b1 is monotone )
proof
let x, y be Element of (ClOpers L); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (ClImageMap L) . x <= (ClImageMap L) . y )
reconsider c = x, d = y as closure Function of L,L by Th10;
A1: (ClImageMap L) . y = Image d by Def4;
assume  x <= y ; ::_thesis: (ClImageMap L) . x <= (ClImageMap L) . y
then  c <= d by Th12;
then A2: Image d is SubRelStr of Image c by Th14;
 (ClImageMap L) . x = Image c by Def4;
then  ~ ((ClImageMap L) . x) >= ~ ((ClImageMap L) . y) by A2, A1, Th17;
hence  (ClImageMap L) . x <= (ClImageMap L) . y by YELLOW_7:1; ::_thesis: verum
end;
take  g ; ::_thesis: ( g = (ClImageMap L) " & g is monotone )
thus  g = (ClImageMap L) " ; ::_thesis: g is monotone
thus  g is monotone ::_thesis: verum
proof
let x, y be Element of ((ClosureSystems L) opp); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or g . x <= g . y )
reconsider A = ~ x, B = ~ y as strict full infs-inheriting SubRelStr of L by Th16;
A3: B = Image (closure_op B) by Th18;
A4: g . A = closure_op A by Th21;
assume  x <= y ; ::_thesis: g . x <= g . y
then  ~ y <= ~ x by YELLOW_7:1;
then A5: B is SubRelStr of A by Th17;
A6: g . B = closure_op B by Th21;
 A = Image (closure_op A) by Th18;
then  closure_op A <= closure_op B by A5, A3, Th14;
hence  g . x <= g . y by A4, A6, Th12; ::_thesis: verum
end;
end;
case ( ClOpers L is empty or (ClosureSystems L) opp is empty ) ; ::_thesis: ( ClOpers L is empty & (ClosureSystems L) opp is empty )
hence  ( ClOpers L is empty & (ClosureSystems L) opp is empty ) ; ::_thesis: verum
end;
end;
end;
end;

theorem :: WAYBEL10:22
for L being complete LATTICE holds ClOpers L,(ClosureSystems L) opp are_isomorphic
proof
let L be complete LATTICE; ::_thesis: ClOpers L,(ClosureSystems L) opp are_isomorphic
take  ClImageMap L ; :: according to WAYBEL_1:def_8 ::_thesis: ClImageMap L is isomorphic
thus  ClImageMap L is isomorphic ; ::_thesis: verum
end;

begin

theorem Th23: :: WAYBEL10:23
for L being RelStr
for S being full SubRelStr of L
for X being Subset of S holds
( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )
proof
let L be RelStr ; ::_thesis: for S being full SubRelStr of L
for X being Subset of S holds
( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )
let S be full SubRelStr of L; ::_thesis: for X being Subset of S holds
( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )
let X be Subset of S; ::_thesis: ( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )
hereby  ::_thesis: ( X is filtered Subset of L implies X is filtered )
assume A1: X is directed Subset of L ; ::_thesis: X is directed
thus  X is directed ::_thesis: verum
proof
A2: the carrier of S c= the carrier of L by YELLOW_0:def_13;
let x, y be Element of S; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 ) )
assume that
A3: x in X and
A4: y in X ; ::_thesis: ex b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 )
A5: y in the carrier of S by A3;
 x in the carrier of S by A3;
then reconsider x9 = x, y9 = y as Element of L by A5, A2;
consider z being Element of L such that
A6: z in X and
A7: z >= x9 and
A8: z >= y9 by A1, A3, A4, WAYBEL_0:def_1;
reconsider z = z as Element of S by A6;
take  z ; ::_thesis: ( z in X & x <= z & y <= z )
thus  ( z in X & x <= z & y <= z ) by A6, A7, A8, YELLOW_0:60; ::_thesis: verum
end;
end;
assume A9: X is filtered Subset of L ; ::_thesis: X is filtered
A10: the carrier of S c= the carrier of L by YELLOW_0:def_13;
let x, y be Element of S; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of S st
( b1 in X & b1 <= x & b1 <= y ) )
assume that
A11: x in X and
A12: y in X ; ::_thesis: ex b1 being Element of the carrier of S st
( b1 in X & b1 <= x & b1 <= y )
A13: y in the carrier of S by A11;
 x in the carrier of S by A11;
then reconsider x9 = x, y9 = y as Element of L by A13, A10;
consider z being Element of L such that
A14: z in X and
A15: z <= x9 and
A16: z <= y9 by A9, A11, A12, WAYBEL_0:def_2;
reconsider z = z as Element of S by A14;
take  z ; ::_thesis: ( z in X & z <= x & z <= y )
thus  ( z in X & z <= x & z <= y ) by A14, A15, A16, YELLOW_0:60; ::_thesis: verum
end;

theorem Th24: :: WAYBEL10:24
for L being complete LATTICE
for S being closure System of L holds
( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )
proof
let L be complete LATTICE; ::_thesis: for S being closure System of L holds
( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )
let S be closure System of L; ::_thesis: ( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )
set c = closure_op S;
A1: Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #) by Th18;
hereby  ::_thesis: ( S is directed-sups-inheriting implies closure_op S is directed-sups-preserving )
set Lk =  {  k where k is Element of L : (closure_op S) . k <= k  }  ;
set k = the Element of L;
A2:  {  k where k is Element of L : (closure_op S) . k <= k  }  c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  k where k is Element of L : (closure_op S) . k <= k  }  or x in the carrier of L )
assume  x in  {  k where k is Element of L : (closure_op S) . k <= k  }  ; ::_thesis: x in the carrier of L
then  ex k being Element of L st
( x = k & (closure_op S) . k <= k ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
 (closure_op S) . ((closure_op S) . the Element of L) = (closure_op S) . the Element of L by YELLOW_2:18;
then A3: (closure_op S) . the Element of L in  {  k where k is Element of L : (closure_op S) . k <= k  }  ;
assume  closure_op S is directed-sups-preserving ; ::_thesis: S is directed-sups-inheriting
then A4: Image (closure_op S) is directed-sups-inheriting by A3, A2, WAYBEL_1:52;
thus  S is directed-sups-inheriting ::_thesis: verum
proof
let X be directed Subset of S; :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of S )
assume that
A5: X <> {} and
A6: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of S
reconsider Y = X as Subset of (Image (closure_op S)) by A1;
 Y is directed by A1, WAYBEL_0:3;
hence  "\/" (X,L) in the carrier of S by A1, A4, A5, A6, WAYBEL_0:def_4; ::_thesis: verum
end;
end;
assume A7: for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of S ; :: according to WAYBEL_0:def_4 ::_thesis: closure_op S is directed-sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or closure_op S preserves_sup_of X )
assume A8: ( not X is empty & X is directed ) ; ::_thesis: closure_op S preserves_sup_of X
 rng (closure_op S) = the carrier of S by A1, YELLOW_0:def_15;
then reconsider Y = (closure_op S) .: X as Subset of S by RELAT_1:111;
assume  ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (closure_op S) .: X,L & "\/" (((closure_op S) .: X),L) = (closure_op S) . ("\/" (X,L)) )
thus  ex_sup_of (closure_op S) .: X,L by YELLOW_0:17; ::_thesis: "\/" (((closure_op S) .: X),L) = (closure_op S) . ("\/" (X,L))
 (closure_op S) .: X is_<=_than (closure_op S) . (sup X)
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in (closure_op S) .: X or x <= (closure_op S) . (sup X) )
assume  x in (closure_op S) .: X ; ::_thesis: x <= (closure_op S) . (sup X)
then consider a being set  such that
A9: a in the carrier of L and
A10: a in X and
A11: x = (closure_op S) . a by FUNCT_2:64;
reconsider a = a as Element of L by A9;
 a <= sup X by A10, YELLOW_2:22;
hence  x <= (closure_op S) . (sup X) by A11, WAYBEL_1:def_2; ::_thesis: verum
end;
then A12: sup ((closure_op S) .: X) <= (closure_op S) . (sup X) by YELLOW_0:32;
 X is_<=_than sup ((closure_op S) .: X)
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= sup ((closure_op S) .: X) )
assume  x in X ; ::_thesis: x <= sup ((closure_op S) .: X)
then  (closure_op S) . x in (closure_op S) .: X by FUNCT_2:35;
then A13: (closure_op S) . x <= sup ((closure_op S) .: X) by YELLOW_2:22;
 x <= (closure_op S) . x by Th5;
hence  x <= sup ((closure_op S) .: X) by A13, ORDERS_2:3; ::_thesis: verum
end;
then A14: sup X <= sup ((closure_op S) .: X) by YELLOW_0:32;
set x = the Element of X;
 the Element of X in X by A8;
then A15: (closure_op S) . the Element of X in (closure_op S) .: X by FUNCT_2:35;
 Y is directed by A8, Th23, YELLOW_2:15;
then  sup ((closure_op S) .: X) in the carrier of S by A7, A15, YELLOW_0:17;
then  ex a being Element of L st (closure_op S) . a = sup ((closure_op S) .: X) by A1, YELLOW_2:10;
then  (closure_op S) . (sup ((closure_op S) .: X)) = sup ((closure_op S) .: X) by YELLOW_2:18;
then  (closure_op S) . (sup X) <= sup ((closure_op S) .: X) by A14, WAYBEL_1:def_2;
hence  "\/" (((closure_op S) .: X),L) = (closure_op S) . ("\/" (X,L)) by A12, ORDERS_2:2; ::_thesis: verum
end;

theorem :: WAYBEL10:25
for L being complete LATTICE
for h being closure Function of L,L holds
( h is directed-sups-preserving iff Image h is directed-sups-inheriting )
proof
let L be complete LATTICE; ::_thesis: for h being closure Function of L,L holds
( h is directed-sups-preserving iff Image h is directed-sups-inheriting )
let h be closure Function of L,L; ::_thesis: ( h is directed-sups-preserving iff Image h is directed-sups-inheriting )
 closure_op (Image h) = h by Th19;
hence  ( h is directed-sups-preserving iff Image h is directed-sups-inheriting ) by Th24; ::_thesis: verum
end;

registration
let L be complete LATTICE;
let S be closure directed-sups-inheriting System of L;
cluster closure_op S ->  directed-sups-preserving ;
coherence
 closure_op S is directed-sups-preserving by Th24;
end;

registration
let L be complete LATTICE;
let h be directed-sups-preserving closure Function of L,L;
cluster Image h ->  directed-sups-inheriting ;
coherence
 Image h is directed-sups-inheriting
proof
 h = closure_op (Image h) by Th19;
hence  Image h is directed-sups-inheriting by Th24; ::_thesis: verum
end;
end;

definition
let L be non empty reflexive RelStr ;
func DsupClOpers L ->  non empty strict full SubRelStr of ClOpers L means :Def6: :: WAYBEL10:def 6
 for f being closure Function of L,L holds
( f is Element of it iff f is directed-sups-preserving );
existence
 ex b1 being non empty strict full SubRelStr of ClOpers L st
for f being closure Function of L,L holds
( f is Element of b1 iff f is directed-sups-preserving )
proof
defpred S1[ set ] means $1 is directed-sups-preserving Function of L,L;
set h = the directed-sups-preserving closure Function of L,L;
 the directed-sups-preserving closure Function of L,L is Element of (ClOpers L) by Def1;
then A1: the directed-sups-preserving closure Function of L,L in the carrier of (ClOpers L) ;
A2: S1[ the directed-sups-preserving closure Function of L,L] ;
consider S being non empty strict full SubRelStr of ClOpers L such that
A3: for f being Element of (ClOpers L) holds
( f is Element of S iff S1[f] ) from WAYBEL10:sch_1(A2, A1);
take  S ; ::_thesis: for f being closure Function of L,L holds
( f is Element of S iff f is directed-sups-preserving )
let f be closure Function of L,L; ::_thesis: ( f is Element of S iff f is directed-sups-preserving )
hereby  ::_thesis: ( f is directed-sups-preserving implies f is Element of S )
assume A4: f is Element of S ; ::_thesis: f is directed-sups-preserving
then  f is Element of (ClOpers L) by YELLOW_0:58;
hence  f is directed-sups-preserving by A3, A4; ::_thesis: verum
end;
assume A5: f is directed-sups-preserving ; ::_thesis: f is Element of S
 f is Element of (ClOpers L) by Def1;
hence  f is Element of S by A3, A5; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of ClOpers L st ( for f being closure Function of L,L holds
( f is Element of b1 iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds
( f is Element of b2 iff f is directed-sups-preserving ) ) holds
b1 = b2;
proof
defpred S1[ set ] means $1 is directed-sups-preserving closure Function of L,L;
let S1, S2 be non empty strict full SubRelStr of ClOpers L; ::_thesis: ( ( for f being closure Function of L,L holds
( f is Element of S1 iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds
( f is Element of S2 iff f is directed-sups-preserving ) ) implies S1 = S2 )
assume that
A6: for f being closure Function of L,L holds
( f is Element of S1 iff f is directed-sups-preserving ) and
A7: for f being closure Function of L,L holds
( f is Element of S2 iff f is directed-sups-preserving ) ; ::_thesis: S1 = S2
A8: now__::_thesis:_for_f_being_set_holds_
(_f_is_Element_of_S2_iff_S1[f]_)
let f be set ; ::_thesis: ( f is Element of S2 iff S1[f] )
 ( f is Element of S2 implies f is Element of (ClOpers L) ) by YELLOW_0:58;
then  ( f is Element of S2 implies f is closure Function of L,L ) by Th10;
hence  ( f is Element of S2 iff S1[f] ) by A7; ::_thesis: verum
end;
A9: now__::_thesis:_for_f_being_set_holds_
(_f_is_Element_of_S1_iff_S1[f]_)
let f be set ; ::_thesis: ( f is Element of S1 iff S1[f] )
 ( f is Element of S1 implies f is Element of (ClOpers L) ) by YELLOW_0:58;
then  ( f is Element of S1 implies f is closure Function of L,L ) by Th10;
hence  ( f is Element of S1 iff S1[f] ) by A6; ::_thesis: verum
end;
 RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch_3(A9, A8);
hence  S1 = S2 ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines DsupClOpers WAYBEL10:def_6_:_
 for L being non empty reflexive RelStr
for b2 being non empty strict full SubRelStr of ClOpers L holds
( b2 = DsupClOpers L iff for f being closure Function of L,L holds
( f is Element of b2 iff f is directed-sups-preserving ) );

theorem Th26: :: WAYBEL10:26
for L being non empty reflexive RelStr
for x being set holds
( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L )
proof
let L be non empty reflexive RelStr ; ::_thesis: for x being set holds
( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L )
let x be set ; ::_thesis: ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L )
 ( x is Element of (ClOpers L) iff x is closure Function of L,L ) by Th10;
hence  ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L ) by Def6, YELLOW_0:58; ::_thesis: verum
end;

definition
let L be non empty RelStr ;
func Subalgebras L ->  non empty strict full SubRelStr of ClosureSystems L means :Def7: :: WAYBEL10:def 7
 for R being strict closure System of L holds
( R is Element of it iff R is directed-sups-inheriting );
existence
 ex b1 being non empty strict full SubRelStr of ClosureSystems L st
for R being strict closure System of L holds
( R is Element of b1 iff R is directed-sups-inheriting )
proof
defpred S1[ set ] means $1 is directed-sups-inheriting SubRelStr of L;
set SL = subrelstr ([#] L);
 subrelstr ([#] L) is Element of (ClosureSystems L) by Def3;
then A1: subrelstr ([#] L) in the carrier of (ClosureSystems L) ;
A2: S1[ subrelstr ([#] L)] ;
consider S being non empty strict full SubRelStr of ClosureSystems L such that
A3: for x being Element of (ClosureSystems L) holds
( x is Element of S iff S1[x] ) from WAYBEL10:sch_1(A2, A1);
take  S ; ::_thesis: for R being strict closure System of L holds
( R is Element of S iff R is directed-sups-inheriting )
let R be strict closure System of L; ::_thesis: ( R is Element of S iff R is directed-sups-inheriting )
 R is Element of (ClosureSystems L) by Def3;
hence  ( R is Element of S iff R is directed-sups-inheriting ) by A3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of ClosureSystems L st ( for R being strict closure System of L holds
( R is Element of b1 iff R is directed-sups-inheriting ) ) & ( for R being strict closure System of L holds
( R is Element of b2 iff R is directed-sups-inheriting ) ) holds
b1 = b2;
proof
defpred S1[ set ] means $1 is strict closure directed-sups-inheriting System of L;
let S1, S2 be non empty strict full SubRelStr of ClosureSystems L; ::_thesis: ( ( for R being strict closure System of L holds
( R is Element of S1 iff R is directed-sups-inheriting ) ) & ( for R being strict closure System of L holds
( R is Element of S2 iff R is directed-sups-inheriting ) ) implies S1 = S2 )
assume that
A4: for R being strict closure System of L holds
( R is Element of S1 iff R is directed-sups-inheriting ) and
A5: for R being strict closure System of L holds
( R is Element of S2 iff R is directed-sups-inheriting ) ; ::_thesis: S1 = S2
A6: now__::_thesis:_for_x_being_set_holds_
(_x_is_Element_of_S2_iff_S1[x]_)
let x be set ; ::_thesis: ( x is Element of S2 iff S1[x] )
 ( x is Element of S2 implies x is Element of (ClosureSystems L) ) by YELLOW_0:58;
then  ( x is Element of S2 implies x is strict closure System of L ) by Th16;
hence  ( x is Element of S2 iff S1[x] ) by A5; ::_thesis: verum
end;
A7: now__::_thesis:_for_x_being_set_holds_
(_x_is_Element_of_S1_iff_S1[x]_)
let x be set ; ::_thesis: ( x is Element of S1 iff S1[x] )
 ( x is Element of S1 implies x is Element of (ClosureSystems L) ) by YELLOW_0:58;
then  ( x is Element of S1 implies x is strict closure System of L ) by Th16;
hence  ( x is Element of S1 iff S1[x] ) by A4; ::_thesis: verum
end;
 RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) from WAYBEL10:sch_3(A7, A6);
hence  S1 = S2 ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Subalgebras WAYBEL10:def_7_:_
 for L being non empty RelStr
for b2 being non empty strict full SubRelStr of ClosureSystems L holds
( b2 = Subalgebras L iff for R being strict closure System of L holds
( R is Element of b2 iff R is directed-sups-inheriting ) );

theorem Th27: :: WAYBEL10:27
for L being non empty RelStr
for x being set holds
( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )
proof
let L be non empty RelStr ; ::_thesis: for x being set holds
( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )
let x be set ; ::_thesis: ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )
 ( x is Element of (ClosureSystems L) iff x is strict closure System of L ) by Th16;
hence  ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L ) by Def7, YELLOW_0:58; ::_thesis: verum
end;

theorem Th28: :: WAYBEL10:28
for L being complete LATTICE holds Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp
proof
let L be complete LATTICE; ::_thesis: Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp
defpred S1[ set ] means $1 is strict closure directed-sups-inheriting System of L;
A1: now__::_thesis:_for_a_being_set_holds_
(_(_a_is_Element_of_(Image_((ClImageMap_L)_|_(DsupClOpers_L)))_implies_S1[a]_)_&_(_S1[a]_implies_a_is_Element_of_(Image_((ClImageMap_L)_|_(DsupClOpers_L)))_)_)
let a be set ; ::_thesis: ( ( a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) implies S1[a] ) & ( S1[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ) )
hereby  ::_thesis: ( S1[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) )
assume  a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ; ::_thesis: S1[a]
then consider x being Element of (DsupClOpers L) such that
A2: ((ClImageMap L) | (DsupClOpers L)) . x = a by YELLOW_2:10;
reconsider x = x as directed-sups-preserving closure Function of L,L by Th26;
a = (ClImageMap L) . x by A2, Th6
.= Image x by Def4 ;
hence  S1[a] ; ::_thesis: verum
end;
assume  S1[a] ; ::_thesis: a is Element of (Image ((ClImageMap L) | (DsupClOpers L)))
then reconsider S = a as strict closure directed-sups-inheriting System of L ;
reconsider x = closure_op S as Element of (DsupClOpers L) by Th26;
S = Image (closure_op S) by Th18
.= (ClImageMap L) . (closure_op S) by Def4
.= ((ClImageMap L) | (DsupClOpers L)) . x by Th6 ;
then  S in rng ((ClImageMap L) | (DsupClOpers L)) by FUNCT_2:4;
hence  a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) by YELLOW_0:def_15; ::_thesis: verum
end;
A3: for a being set holds
( a is Element of ((Subalgebras L) opp) iff S1[a] ) by Th27;
 RelStr(# the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the InternalRel of (Image ((ClImageMap L) | (DsupClOpers L))) #) = RelStr(# the carrier of ((Subalgebras L) opp), the InternalRel of ((Subalgebras L) opp) #) from WAYBEL10:sch_3(A1, A3);
hence  Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp ; ::_thesis: verum
end;

registration
let L be complete LATTICE;
cluster corestr ((ClImageMap L) | (DsupClOpers L)) ->  isomorphic ;
coherence
 corestr ((ClImageMap L) | (DsupClOpers L)) is isomorphic
proof
set f = ClImageMap L;
set R = DsupClOpers L;
set g = corestr ((ClImageMap L) | (DsupClOpers L));
percases ( ( not DsupClOpers L is empty & not Image ((ClImageMap L) | (DsupClOpers L)) is empty ) or DsupClOpers L is empty or Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ;
:: according to WAYBEL_0:def_38
case ( not DsupClOpers L is empty & not Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; ::_thesis: ( corestr ((ClImageMap L) | (DsupClOpers L)) is one-to-one & corestr ((ClImageMap L) | (DsupClOpers L)) is monotone & ex b1 being Element of bool [: the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the carrier of (DsupClOpers L):] st
( b1 = (corestr ((ClImageMap L) | (DsupClOpers L))) " & b1 is monotone ) )
 (ClImageMap L) | (DsupClOpers L) is V7() by Th7;
hence  ( corestr ((ClImageMap L) | (DsupClOpers L)) is V7() & corestr ((ClImageMap L) | (DsupClOpers L)) is monotone ) by WAYBEL_1:30; ::_thesis: ex b1 being Element of bool [: the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the carrier of (DsupClOpers L):] st
( b1 = (corestr ((ClImageMap L) | (DsupClOpers L))) " & b1 is monotone )
consider f9 being Function of ((ClosureSystems L) opp),(ClOpers L) such that
A1: f9 = (ClImageMap L) " and
 f9 is monotone by WAYBEL_0:def_38;
reconsider h = f9 | (Image ((ClImageMap L) | (DsupClOpers L))) as Function of (Image ((ClImageMap L) | (DsupClOpers L))),(DsupClOpers L) by A1, Th8;
take  h ; ::_thesis: ( h = (corestr ((ClImageMap L) | (DsupClOpers L))) " & h is monotone )
thus h = ((ClImageMap L) | (DsupClOpers L)) " by A1, Th8
.= (corestr ((ClImageMap L) | (DsupClOpers L))) " by WAYBEL_1:30 ; ::_thesis: h is monotone
let x, y be Element of (Image ((ClImageMap L) | (DsupClOpers L))); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or h . x <= h . y )
reconsider a = x, b = y as Element of ((ClosureSystems L) opp) by YELLOW_0:58;
reconsider A = ~ a, B = ~ b as strict closure System of L by Th16;
reconsider i = closure_op A, j = closure_op B as Element of (ClOpers L) by Th10;
 f9 . y = j by A1, Th21;
then A2: h . y = j by Th6;
assume  x <= y ; ::_thesis: h . x <= h . y
then  a <= b by YELLOW_0:59;
then  ~ a >= ~ b by YELLOW_7:1;
then A3: B is SubRelStr of A by Th17;
A4: B = Image (closure_op B) by Th18;
 A = Image (closure_op A) by Th18;
then  closure_op A <= closure_op B by A3, A4, Th14;
then A5: i <= j by Th12;
 f9 . x = i by A1, Th21;
then  h . x = i by Th6;
hence  h . x <= h . y by A2, A5, YELLOW_0:60; ::_thesis: verum
end;
case ( DsupClOpers L is empty or Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; ::_thesis: ( DsupClOpers L is empty & Image ((ClImageMap L) | (DsupClOpers L)) is empty )
hence  ( DsupClOpers L is empty & Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; ::_thesis: verum
end;
end;
end;
end;

theorem :: WAYBEL10:29
for L being complete LATTICE holds DsupClOpers L,(Subalgebras L) opp are_isomorphic
proof
let L be complete LATTICE; ::_thesis: DsupClOpers L,(Subalgebras L) opp are_isomorphic
set f = (ClImageMap L) | (DsupClOpers L);
reconsider g = corestr ((ClImageMap L) | (DsupClOpers L)) as Function of (DsupClOpers L),((Subalgebras L) opp) by Th28;
take  g ; :: according to WAYBEL_1:def_8 ::_thesis: g is isomorphic
 Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp by Th28;
hence  g is isomorphic ; ::_thesis: verum
end;