:: WAYBEL_4 semantic presentation

begin

definition
let L be non empty reflexive RelStr ;
funcL -waybelow  ->  Relation of L means :Def1: :: WAYBEL_4:def 1
 for x, y being Element of L holds
( [x,y] in it iff x << y );
existence
 ex b1 being Relation of L st
for x, y being Element of L holds
( [x,y] in b1 iff x << y )
proof
defpred S1[ set , set ] means  ex x9, y9 being Element of L st
( x9 = $1 & y9 = $2 & x9 << y9 );
consider R being Relation of the carrier of L, the carrier of L such that
A1: for x, y being set holds
( [x,y] in R iff ( x in the carrier of L & y in the carrier of L & S1[x,y] ) ) from RELSET_1:sch_1();
reconsider R = R as Relation of L ;
take  R ; ::_thesis: for x, y being Element of L holds
( [x,y] in R iff x << y )
let x, y be Element of L; ::_thesis: ( [x,y] in R iff x << y )
hereby  ::_thesis: ( x << y implies [x,y] in R )
assume  [x,y] in R ; ::_thesis: x << y
then  ex x9, y9 being Element of L st
( x9 = x & y9 = y & x9 << y9 ) by A1;
hence  x << y ; ::_thesis: verum
end;
assume  x << y ; ::_thesis: [x,y] in R
hence  [x,y] in R by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of L st ( for x, y being Element of L holds
( [x,y] in b1 iff x << y ) ) & ( for x, y being Element of L holds
( [x,y] in b2 iff x << y ) ) holds
b1 = b2
proof
let A1, A2 be Relation of L; ::_thesis: ( ( for x, y being Element of L holds
( [x,y] in A1 iff x << y ) ) & ( for x, y being Element of L holds
( [x,y] in A2 iff x << y ) ) implies A1 = A2 )
assume A2: for x, y being Element of L holds
( [x,y] in A1 iff x << y ) ; ::_thesis: ( ex x, y being Element of L st
( ( [x,y] in A2 implies x << y ) implies ( x << y & not [x,y] in A2 ) ) or A1 = A2 )
assume A3: for x, y being Element of L holds
( [x,y] in A2 iff x << y ) ; ::_thesis: A1 = A2
thus  A1 = A2 ::_thesis: verum
proof
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in A1 or [a,b] in A2 ) & ( not [a,b] in A2 or [a,b] in A1 ) )
hereby  ::_thesis: ( not [a,b] in A2 or [a,b] in A1 )
assume A4: [a,b] in A1 ; ::_thesis: [a,b] in A2
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
 a9 << b9 by A2, A4;
hence  [a,b] in A2 by A3; ::_thesis: verum
end;
assume A5: [a,b] in A2 ; ::_thesis: [a,b] in A1
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
 a9 << b9 by A3, A5;
hence  [a,b] in A1 by A2; ::_thesis: verum
end;
end;
end;

:: deftheorem Def1 defines -waybelow WAYBEL_4:def_1_:_
 for L being non empty reflexive RelStr
for b2 being Relation of L holds
( b2 = L -waybelow iff for x, y being Element of L holds
( [x,y] in b2 iff x << y ) );

definition
let L be RelStr ;
func IntRel L ->  Relation of L equals :: WAYBEL_4:def 2
 the InternalRel of L;
coherence
 the InternalRel of L is Relation of L ;
correctness
;
end;

:: deftheorem  defines IntRel WAYBEL_4:def_2_:_
 for L being RelStr holds IntRel L = the InternalRel of L;

definition
let L be RelStr ;
let R be Relation of L;
attrR is auxiliary(i)  means :Def3: :: WAYBEL_4:def 3
 for x, y being Element of L st [x,y] in R holds
x <= y;
attrR is auxiliary(ii)  means :Def4: :: WAYBEL_4:def 4
 for x, y, z, u being Element of L st u <= x & [x,y] in R & y <= z holds
[u,z] in R;
end;

:: deftheorem Def3 defines auxiliary(i) WAYBEL_4:def_3_:_
 for L being RelStr
for R being Relation of L holds
( R is auxiliary(i) iff for x, y being Element of L st [x,y] in R holds
x <= y );

:: deftheorem Def4 defines auxiliary(ii) WAYBEL_4:def_4_:_
 for L being RelStr
for R being Relation of L holds
( R is auxiliary(ii) iff for x, y, z, u being Element of L st u <= x & [x,y] in R & y <= z holds
[u,z] in R );

definition
let L be non empty RelStr ;
let R be Relation of L;
attrR is auxiliary(iii)  means :Def5: :: WAYBEL_4:def 5
 for x, y, z being Element of L st [x,z] in R & [y,z] in R holds
[(x "\/" y),z] in R;
attrR is auxiliary(iv)  means :Def6: :: WAYBEL_4:def 6
 for x being Element of L holds [(Bottom L),x] in R;
end;

:: deftheorem Def5 defines auxiliary(iii) WAYBEL_4:def_5_:_
 for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary(iii) iff for x, y, z being Element of L st [x,z] in R & [y,z] in R holds
[(x "\/" y),z] in R );

:: deftheorem Def6 defines auxiliary(iv) WAYBEL_4:def_6_:_
 for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary(iv) iff for x being Element of L holds [(Bottom L),x] in R );

definition
let L be non empty RelStr ;
let R be Relation of L;
attrR is auxiliary  means :Def7: :: WAYBEL_4:def 7
( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) );
end;

:: deftheorem Def7 defines auxiliary WAYBEL_4:def_7_:_
 for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) ) );

registration
let L be non empty RelStr ;
cluster auxiliary  ->  auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:];
coherence
 for b1 being Relation of L st b1 is auxiliary holds
( b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iii) & b1 is auxiliary(iv) ) by Def7;
cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv)  ->  auxiliary for Element of bool [: the carrier of L, the carrier of L:];
coherence
 for b1 being Relation of L st b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iii) & b1 is auxiliary(iv) holds
b1 is auxiliary by Def7;
end;

registration
let L be transitive antisymmetric lower-bounded with_suprema RelStr ;
cluster Relation-like auxiliary for Element of bool [: the carrier of L, the carrier of L:];
existence
 ex b1 being Relation of L st b1 is auxiliary
proof
set A = IntRel L;
take  IntRel L ; ::_thesis: IntRel L is auxiliary
thus  IntRel L is auxiliary(i) :: according to WAYBEL_4:def_7 ::_thesis: ( IntRel L is auxiliary(ii) & IntRel L is auxiliary(iii) & IntRel L is auxiliary(iv) )
proof
let x, y be Element of L; :: according to WAYBEL_4:def_3 ::_thesis: ( [x,y] in IntRel L implies x <= y )
assume  [x,y] in IntRel L ; ::_thesis: x <= y
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
thus  IntRel L is auxiliary(ii) ::_thesis: ( IntRel L is auxiliary(iii) & IntRel L is auxiliary(iv) )
proof
let x, y, z, u be Element of L; :: according to WAYBEL_4:def_4 ::_thesis: ( u <= x & [x,y] in IntRel L & y <= z implies [u,z] in IntRel L )
assume that
A1: u <= x and
A2: [x,y] in IntRel L and
A3: y <= z ; ::_thesis: [u,z] in IntRel L
 x <= y by A2, ORDERS_2:def_5;
then  u <= y by A1, ORDERS_2:3;
then  u <= z by A3, ORDERS_2:3;
hence  [u,z] in IntRel L by ORDERS_2:def_5; ::_thesis: verum
end;
thus  IntRel L is auxiliary(iii) ::_thesis: IntRel L is auxiliary(iv)
proof
let x, y, z be Element of L; :: according to WAYBEL_4:def_5 ::_thesis: ( [x,z] in IntRel L & [y,z] in IntRel L implies [(x "\/" y),z] in IntRel L )
assume that
A4: [x,z] in IntRel L and
A5: [y,z] in IntRel L ; ::_thesis: [(x "\/" y),z] in IntRel L
A6: x <= z by A4, ORDERS_2:def_5;
A7: y <= z by A5, ORDERS_2:def_5;
 ex q being Element of L st
( x <= q & y <= q & ( for c being Element of L st x <= c & y <= c holds
q <= c ) ) by LATTICE3:def_10;
then  x "\/" y <= z by A6, A7, LATTICE3:def_13;
hence  [(x "\/" y),z] in IntRel L by ORDERS_2:def_5; ::_thesis: verum
end;
thus  IntRel L is auxiliary(iv) ::_thesis: verum
proof
let x be Element of L; :: according to WAYBEL_4:def_6 ::_thesis: [(Bottom L),x] in IntRel L
 Bottom L <= x by YELLOW_0:44;
hence  [(Bottom L),x] in IntRel L by ORDERS_2:def_5; ::_thesis: verum
end;
end;
end;

theorem Th1: :: WAYBEL_4:1
for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) auxiliary(iii) Relation of L
for x, y, z, u being Element of L st [x,z] in AR & [y,u] in AR holds
[(x "\/" y),(z "\/" u)] in AR
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary(ii) auxiliary(iii) Relation of L
for x, y, z, u being Element of L st [x,z] in AR & [y,u] in AR holds
[(x "\/" y),(z "\/" u)] in AR
let AR be auxiliary(ii) auxiliary(iii) Relation of L; ::_thesis: for x, y, z, u being Element of L st [x,z] in AR & [y,u] in AR holds
[(x "\/" y),(z "\/" u)] in AR
let x, y, z, u be Element of L; ::_thesis: ( [x,z] in AR & [y,u] in AR implies [(x "\/" y),(z "\/" u)] in AR )
assume that
A1: [x,z] in AR and
A2: [y,u] in AR ; ::_thesis: [(x "\/" y),(z "\/" u)] in AR
A3: x <= x ;
A4: y <= y ;
A5: z <= z "\/" u by YELLOW_0:22;
A6: u <= z "\/" u by YELLOW_0:22;
A7: [x,(z "\/" u)] in AR by A1, A3, A5, Def4;
 [y,(z "\/" u)] in AR by A2, A4, A6, Def4;
hence  [(x "\/" y),(z "\/" u)] in AR by A7, Def5; ::_thesis: verum
end;

Lm1:  for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) auxiliary(ii) Relation of L holds AR is transitive
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary(i) auxiliary(ii) Relation of L holds AR is transitive
let AR be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: AR is transitive
A1: field AR c= the carrier of L \/ the carrier of L by RELSET_1:8;
now__::_thesis:_for_x,_y,_z_being_set_st_x_in_field_AR_&_y_in_field_AR_&_z_in_field_AR_&_[x,y]_in_AR_&_[y,z]_in_AR_holds_
[x,z]_in_AR
let x, y, z be set ; ::_thesis: ( x in field AR & y in field AR & z in field AR & [x,y] in AR & [y,z] in AR implies [x,z] in AR )
assume that
A2: x in field AR and
A3: y in field AR and
A4: z in field AR and
A5: [x,y] in AR and
A6: [y,z] in AR ; ::_thesis: [x,z] in AR
reconsider x9 = x, y9 = y, z9 = z as Element of L by A1, A2, A3, A4;
reconsider x9 = x9, y9 = y9, z9 = z9 as Element of L ;
A7: x9 <= y9 by A5, Def3;
 z9 <= z9 ;
hence  [x,z] in AR by A6, A7, Def4; ::_thesis: verum
end;
then  AR is_transitive_in field AR by RELAT_2:def_8;
hence  AR is transitive by RELAT_2:def_16; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
cluster auxiliary(i) auxiliary(ii)  ->  transitive for Element of bool [: the carrier of L, the carrier of L:];
coherence
 for b1 being Relation of L st b1 is auxiliary(i) & b1 is auxiliary(ii) holds
b1 is transitive by Lm1;
end;

registration
let L be RelStr ;
cluster IntRel L ->  auxiliary(i) ;
coherence
 IntRel L is auxiliary(i)
proof
let x, y be Element of L; :: according to WAYBEL_4:def_3 ::_thesis: ( [x,y] in IntRel L implies x <= y )
assume  [x,y] in IntRel L ; ::_thesis: x <= y
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
end;

registration
let L be transitive RelStr ;
cluster IntRel L ->  auxiliary(ii) ;
coherence
 IntRel L is auxiliary(ii)
proof
set A = IntRel L;
let x, y, z, u be Element of L; :: according to WAYBEL_4:def_4 ::_thesis: ( u <= x & [x,y] in IntRel L & y <= z implies [u,z] in IntRel L )
assume that
A1: u <= x and
A2: [x,y] in IntRel L and
A3: y <= z ; ::_thesis: [u,z] in IntRel L
 x <= y by A2, ORDERS_2:def_5;
then  u <= y by A1, ORDERS_2:3;
then  u <= z by A3, ORDERS_2:3;
hence  [u,z] in IntRel L by ORDERS_2:def_5; ::_thesis: verum
end;
end;

registration
let L be antisymmetric with_suprema RelStr ;
cluster IntRel L ->  auxiliary(iii) ;
coherence
 IntRel L is auxiliary(iii)
proof
set A = IntRel L;
let x, y, z be Element of L; :: according to WAYBEL_4:def_5 ::_thesis: ( [x,z] in IntRel L & [y,z] in IntRel L implies [(x "\/" y),z] in IntRel L )
assume that
A1: [x,z] in IntRel L and
A2: [y,z] in IntRel L ; ::_thesis: [(x "\/" y),z] in IntRel L
A3: x <= z by A1, ORDERS_2:def_5;
A4: y <= z by A2, ORDERS_2:def_5;
 ex q being Element of L st
( x <= q & y <= q & ( for c being Element of L st x <= c & y <= c holds
q <= c ) ) by LATTICE3:def_10;
then  x "\/" y <= z by A3, A4, LATTICE3:def_13;
hence  [(x "\/" y),z] in IntRel L by ORDERS_2:def_5; ::_thesis: verum
end;
end;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
cluster IntRel L ->  auxiliary(iv) ;
coherence
 IntRel L is auxiliary(iv)
proof
set A = IntRel L;
 for x being Element of L holds [(Bottom L),x] in IntRel L
proof
let x be Element of L; ::_thesis: [(Bottom L),x] in IntRel L
 Bottom L <= x by YELLOW_0:44;
hence  [(Bottom L),x] in IntRel L by ORDERS_2:def_5; ::_thesis: verum
end;
hence  IntRel L is auxiliary(iv) by Def6; ::_thesis: verum
end;
end;

definition
let L be lower-bounded sup-Semilattice;
func Aux L ->  set  means :Def8: :: WAYBEL_4:def 8
 for a being set holds
( a in it iff a is auxiliary Relation of L );
existence
 ex b1 being set st
for a being set holds
( a in b1 iff a is auxiliary Relation of L )
proof
defpred S1[ set ] means $1 is auxiliary Relation of L;
consider X being set  such that
A1: for a being set holds
( a in X iff ( a in bool [: the carrier of L, the carrier of L:] & S1[a] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for a being set holds
( a in X iff a is auxiliary Relation of L )
thus  for a being set holds
( a in X iff a is auxiliary Relation of L ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for a being set holds
( a in b1 iff a is auxiliary Relation of L ) ) & ( for a being set holds
( a in b2 iff a is auxiliary Relation of L ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for a being set holds
( a in A1 iff a is auxiliary Relation of L ) ) & ( for a being set holds
( a in A2 iff a is auxiliary Relation of L ) ) implies A1 = A2 )
assume that
A2: for a being set holds
( a in A1 iff a is auxiliary Relation of L ) and
A3: for a being set holds
( a in A2 iff a is auxiliary Relation of L ) ; ::_thesis: A1 = A2
thus  A1 = A2 ::_thesis: verum
proof
thus  A1 c= A2 :: according to XBOOLE_0:def_10 ::_thesis: A2 c= A1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 or a in A2 )
assume  a in A1 ; ::_thesis: a in A2
then  a is auxiliary Relation of L by A2;
hence  a in A2 by A3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A2 or a in A1 )
assume  a in A2 ; ::_thesis: a in A1
then  a is auxiliary Relation of L by A3;
hence  a in A1 by A2; ::_thesis: verum
end;
end;
end;

:: deftheorem Def8 defines Aux WAYBEL_4:def_8_:_
 for L being lower-bounded sup-Semilattice
for b2 being set holds
( b2 = Aux L iff for a being set holds
( a in b2 iff a is auxiliary Relation of L ) );

registration
let L be lower-bounded sup-Semilattice;
cluster Aux L ->  non empty ;
coherence
 not Aux L is empty
proof
 IntRel L is auxiliary Relation of L ;
hence  not Aux L is empty by Def8; ::_thesis: verum
end;
end;

Lm2:  for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L
for a, b being set st [a,b] in AR holds
[a,b] in IntRel L
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary(i) Relation of L
for a, b being set st [a,b] in AR holds
[a,b] in IntRel L
let AR be auxiliary(i) Relation of L; ::_thesis: for a, b being set st [a,b] in AR holds
[a,b] in IntRel L
let a, b be set ; ::_thesis: ( [a,b] in AR implies [a,b] in IntRel L )
assume A1: [a,b] in AR ; ::_thesis: [a,b] in IntRel L
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
 a9 <= b9 by A1, Def3;
hence  [a,b] in IntRel L by ORDERS_2:def_5; ::_thesis: verum
end;

theorem Th2: :: WAYBEL_4:2
for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L holds AR c= IntRel L
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary(i) Relation of L holds AR c= IntRel L
let AR be auxiliary(i) Relation of L; ::_thesis: AR c= IntRel L
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in AR or [a,b] in IntRel L )
assume  [a,b] in AR ; ::_thesis: [a,b] in IntRel L
hence  [a,b] in IntRel L by Lm2; ::_thesis: verum
end;

theorem :: WAYBEL_4:3
for L being lower-bounded sup-Semilattice holds Top (InclPoset (Aux L)) = IntRel L
proof
let L be lower-bounded sup-Semilattice; ::_thesis: Top (InclPoset (Aux L)) = IntRel L
 IntRel L = "/\" ({},(InclPoset (Aux L)))
proof
set P = InclPoset (Aux L);
set I = IntRel L;
 IntRel L in Aux L by Def8;
then reconsider I = IntRel L as Element of (InclPoset (Aux L)) by YELLOW_1:1;
A1: I is_<=_than {} by YELLOW_0:6;
 for b being Element of (InclPoset (Aux L)) st b is_<=_than {} holds
I >= b
proof
let b be Element of (InclPoset (Aux L)); ::_thesis: ( b is_<=_than {} implies I >= b )
 b in the carrier of (InclPoset (Aux L)) ;
then  b in Aux L by YELLOW_1:1;
then reconsider b9 = b as auxiliary Relation of L by Def8;
assume  b is_<=_than {} ; ::_thesis: I >= b
 b9 c= I by Th2;
hence  I >= b by YELLOW_1:3; ::_thesis: verum
end;
hence  IntRel L = "/\" ({},(InclPoset (Aux L))) by A1, YELLOW_0:31; ::_thesis: verum
end;
hence  Top (InclPoset (Aux L)) = IntRel L ; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
cluster InclPoset (Aux L) ->  upper-bounded ;
coherence
 InclPoset (Aux L) is upper-bounded
proof
set I = IntRel L;
 IntRel L in Aux L by Def8;
then reconsider I = IntRel L as Element of (InclPoset (Aux L)) by YELLOW_1:1;
take  I ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of (InclPoset (Aux L)) is_<=_than I
 I is_>=_than the carrier of (InclPoset (Aux L))
proof
let b be Element of (InclPoset (Aux L)); :: according to LATTICE3:def_9 ::_thesis: ( not b in the carrier of (InclPoset (Aux L)) or b <= I )
assume  b in the carrier of (InclPoset (Aux L)) ; ::_thesis: b <= I
then  b in Aux L by YELLOW_1:1;
then reconsider b9 = b as auxiliary Relation of L by Def8;
 b9 c= I by Th2;
hence  b <= I by YELLOW_1:3; ::_thesis: verum
end;
hence  the carrier of (InclPoset (Aux L)) is_<=_than I ; ::_thesis: verum
end;
end;

definition
let L be non empty RelStr ;
func AuxBottom L ->  Relation of L means :Def9: :: WAYBEL_4:def 9
 for x, y being Element of L holds
( [x,y] in it iff x = Bottom L );
existence
 ex b1 being Relation of L st
for x, y being Element of L holds
( [x,y] in b1 iff x = Bottom L )
proof
defpred S1[ set , set ] means $1 = Bottom L;
consider R being Relation of the carrier of L, the carrier of L such that
A1: for a, b being set holds
( [a,b] in R iff ( a in the carrier of L & b in the carrier of L & S1[a,b] ) ) from RELSET_1:sch_1();
reconsider R = R as Relation of L ;
take  R ; ::_thesis: for x, y being Element of L holds
( [x,y] in R iff x = Bottom L )
let x, y be Element of L; ::_thesis: ( [x,y] in R iff x = Bottom L )
thus  ( [x,y] in R implies x = Bottom L ) by A1; ::_thesis: ( x = Bottom L implies [x,y] in R )
assume  x = Bottom L ; ::_thesis: [x,y] in R
hence  [x,y] in R by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of L st ( for x, y being Element of L holds
( [x,y] in b1 iff x = Bottom L ) ) & ( for x, y being Element of L holds
( [x,y] in b2 iff x = Bottom L ) ) holds
b1 = b2
proof
let A1, A2 be Relation of L; ::_thesis: ( ( for x, y being Element of L holds
( [x,y] in A1 iff x = Bottom L ) ) & ( for x, y being Element of L holds
( [x,y] in A2 iff x = Bottom L ) ) implies A1 = A2 )
assume A2: for x, y being Element of L holds
( [x,y] in A1 iff x = Bottom L ) ; ::_thesis: ( ex x, y being Element of L st
( ( [x,y] in A2 implies x = Bottom L ) implies ( x = Bottom L & not [x,y] in A2 ) ) or A1 = A2 )
assume A3: for x, y being Element of L holds
( [x,y] in A2 iff x = Bottom L ) ; ::_thesis: A1 = A2
thus  A1 = A2 ::_thesis: verum
proof
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in A1 or [a,b] in A2 ) & ( not [a,b] in A2 or [a,b] in A1 ) )
hereby  ::_thesis: ( not [a,b] in A2 or [a,b] in A1 )
assume A4: [a,b] in A1 ; ::_thesis: [a,b] in A2
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
 [a9,b9] in A1 by A4;
then  a9 = Bottom L by A2;
then  [a9,b9] in A2 by A3;
hence  [a,b] in A2 ; ::_thesis: verum
end;
assume A5: [a,b] in A2 ; ::_thesis: [a,b] in A1
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
 [a9,b9] in A2 by A5;
then  a9 = Bottom L by A3;
then  [a9,b9] in A1 by A2;
hence  [a,b] in A1 ; ::_thesis: verum
end;
end;
end;

:: deftheorem Def9 defines AuxBottom WAYBEL_4:def_9_:_
 for L being non empty RelStr
for b2 being Relation of L holds
( b2 = AuxBottom L iff for x, y being Element of L holds
( [x,y] in b2 iff x = Bottom L ) );

registration
let L be lower-bounded sup-Semilattice;
cluster AuxBottom L ->  auxiliary ;
coherence
 AuxBottom L is auxiliary
proof
set A = AuxBottom L;
A1: AuxBottom L is auxiliary(i)
proof
let x, y be Element of L; :: according to WAYBEL_4:def_3 ::_thesis: ( [x,y] in AuxBottom L implies x <= y )
assume  [x,y] in AuxBottom L ; ::_thesis: x <= y
then  x = Bottom L by Def9;
hence  x <= y by YELLOW_0:44; ::_thesis: verum
end;
A2: AuxBottom L is auxiliary(ii)
proof
let x, y, z, u be Element of L; :: according to WAYBEL_4:def_4 ::_thesis: ( u <= x & [x,y] in AuxBottom L & y <= z implies [u,z] in AuxBottom L )
assume that
A3: u <= x and
A4: [x,y] in AuxBottom L and
 y <= z ; ::_thesis: [u,z] in AuxBottom L
A5: x = Bottom L by A4, Def9;
 Bottom L <= u by YELLOW_0:44;
then  u = Bottom L by A3, A5, ORDERS_2:2;
hence  [u,z] in AuxBottom L by Def9; ::_thesis: verum
end;
A6: AuxBottom L is auxiliary(iii)
proof
let x, y, z be Element of L; :: according to WAYBEL_4:def_5 ::_thesis: ( [x,z] in AuxBottom L & [y,z] in AuxBottom L implies [(x "\/" y),z] in AuxBottom L )
assume that
A7: [x,z] in AuxBottom L and
A8: [y,z] in AuxBottom L ; ::_thesis: [(x "\/" y),z] in AuxBottom L
A9: y = Bottom L by A8, Def9;
then  x <= y by A7, Def9;
then  x "\/" y = Bottom L by A9, YELLOW_0:24;
hence  [(x "\/" y),z] in AuxBottom L by Def9; ::_thesis: verum
end;
 for x being Element of L holds [(Bottom L),x] in AuxBottom L by Def9;
then  AuxBottom L is auxiliary(iv) by Def6;
hence  AuxBottom L is auxiliary by A1, A2, A6; ::_thesis: verum
end;
end;

theorem Th4: :: WAYBEL_4:4
for L being lower-bounded sup-Semilattice
for AR being auxiliary(iv) Relation of L holds AuxBottom L c= AR
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for AR being auxiliary(iv) Relation of L holds AuxBottom L c= AR
let AR be auxiliary(iv) Relation of L; ::_thesis: AuxBottom L c= AR
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in AuxBottom L or [a,b] in AR )
assume A1: [a,b] in AuxBottom L ; ::_thesis: [a,b] in AR
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
 [a9,b9] in AuxBottom L by A1;
then  a9 = Bottom L by Def9;
then  [a9,b9] in AR by Def6;
hence  [a,b] in AR ; ::_thesis: verum
end;

theorem :: WAYBEL_4:5
for L being lower-bounded sup-Semilattice holds Bottom (InclPoset (Aux L)) = AuxBottom L
proof
let L be lower-bounded with_suprema Poset; ::_thesis: Bottom (InclPoset (Aux L)) = AuxBottom L
 AuxBottom L in Aux L by Def8;
then reconsider N = AuxBottom L as Element of (InclPoset (Aux L)) by YELLOW_1:1;
A1: N is_>=_than {} by YELLOW_0:6;
 for b being Element of (InclPoset (Aux L)) st b is_>=_than {} holds
N <= b
proof
let b be Element of (InclPoset (Aux L)); ::_thesis: ( b is_>=_than {} implies N <= b )
assume  b is_>=_than {} ; ::_thesis: N <= b
 b in the carrier of (InclPoset (Aux L)) ;
then  b in Aux L by YELLOW_1:1;
then reconsider b9 = b as auxiliary Relation of L by Def8;
 N c= b9 by Th4;
hence  N <= b by YELLOW_1:3; ::_thesis: verum
end;
hence  Bottom (InclPoset (Aux L)) = AuxBottom L by A1, YELLOW_0:30; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
cluster InclPoset (Aux L) ->  lower-bounded ;
coherence
 InclPoset (Aux L) is lower-bounded
proof
set I = AuxBottom L;
 AuxBottom L in Aux L by Def8;
then reconsider I = AuxBottom L as Element of (InclPoset (Aux L)) by YELLOW_1:1;
take  I ; :: according to YELLOW_0:def_4 ::_thesis: I is_<=_than the carrier of (InclPoset (Aux L))
 I is_<=_than the carrier of (InclPoset (Aux L))
proof
let b be Element of (InclPoset (Aux L)); :: according to LATTICE3:def_8 ::_thesis: ( not b in the carrier of (InclPoset (Aux L)) or I <= b )
assume  b in the carrier of (InclPoset (Aux L)) ; ::_thesis: I <= b
then  b in Aux L by YELLOW_1:1;
then reconsider b9 = b as auxiliary Relation of L by Def8;
 I c= b9 by Th4;
hence  I <= b by YELLOW_1:3; ::_thesis: verum
end;
hence  I is_<=_than the carrier of (InclPoset (Aux L)) ; ::_thesis: verum
end;
end;

theorem Th6: :: WAYBEL_4:6
for L being lower-bounded sup-Semilattice
for a, b being auxiliary(i) Relation of L holds a /\ b is auxiliary(i) Relation of L
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for a, b being auxiliary(i) Relation of L holds a /\ b is auxiliary(i) Relation of L
let a, b be auxiliary(i) Relation of L; ::_thesis: a /\ b is auxiliary(i) Relation of L
reconsider ab = a /\ b as Relation of L ;
 for x, y being Element of L st [x,y] in ab holds
x <= y
proof
let x, y be Element of L; ::_thesis: ( [x,y] in ab implies x <= y )
assume  [x,y] in ab ; ::_thesis: x <= y
then  [x,y] in a by XBOOLE_0:def_4;
hence  x <= y by Def3; ::_thesis: verum
end;
hence  a /\ b is auxiliary(i) Relation of L by Def3; ::_thesis: verum
end;

theorem Th7: :: WAYBEL_4:7
for L being lower-bounded sup-Semilattice
for a, b being auxiliary(ii) Relation of L holds a /\ b is auxiliary(ii) Relation of L
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for a, b being auxiliary(ii) Relation of L holds a /\ b is auxiliary(ii) Relation of L
let a, b be auxiliary(ii) Relation of L; ::_thesis: a /\ b is auxiliary(ii) Relation of L
reconsider ab = a /\ b as Relation of L ;
 for x, y, z, u being Element of L st u <= x & [x,y] in ab & y <= z holds
[u,z] in ab
proof
let x, y, z, u be Element of L; ::_thesis: ( u <= x & [x,y] in ab & y <= z implies [u,z] in ab )
assume that
A1: u <= x and
A2: [x,y] in ab and
A3: y <= z ; ::_thesis: [u,z] in ab
A4: [x,y] in a by A2, XBOOLE_0:def_4;
A5: [x,y] in b by A2, XBOOLE_0:def_4;
A6: [u,z] in a by A1, A3, A4, Def4;
 [u,z] in b by A1, A3, A5, Def4;
hence  [u,z] in ab by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  a /\ b is auxiliary(ii) Relation of L by Def4; ::_thesis: verum
end;

theorem Th8: :: WAYBEL_4:8
for L being lower-bounded sup-Semilattice
for a, b being auxiliary(iii) Relation of L holds a /\ b is auxiliary(iii) Relation of L
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for a, b being auxiliary(iii) Relation of L holds a /\ b is auxiliary(iii) Relation of L
let a, b be auxiliary(iii) Relation of L; ::_thesis: a /\ b is auxiliary(iii) Relation of L
reconsider ab = a /\ b as Relation of L ;
 for x, y, z being Element of L st [x,z] in ab & [y,z] in ab holds
[(x "\/" y),z] in ab
proof
let x, y, z be Element of L; ::_thesis: ( [x,z] in ab & [y,z] in ab implies [(x "\/" y),z] in ab )
assume that
A1: [x,z] in ab and
A2: [y,z] in ab ; ::_thesis: [(x "\/" y),z] in ab
A3: [x,z] in a by A1, XBOOLE_0:def_4;
A4: [x,z] in b by A1, XBOOLE_0:def_4;
A5: [y,z] in a by A2, XBOOLE_0:def_4;
A6: [y,z] in b by A2, XBOOLE_0:def_4;
A7: [(x "\/" y),z] in a by A3, A5, Def5;
 [(x "\/" y),z] in b by A4, A6, Def5;
hence  [(x "\/" y),z] in ab by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  a /\ b is auxiliary(iii) Relation of L by Def5; ::_thesis: verum
end;

theorem Th9: :: WAYBEL_4:9
for L being lower-bounded sup-Semilattice
for a, b being auxiliary(iv) Relation of L holds a /\ b is auxiliary(iv) Relation of L
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for a, b being auxiliary(iv) Relation of L holds a /\ b is auxiliary(iv) Relation of L
let a, b be auxiliary(iv) Relation of L; ::_thesis: a /\ b is auxiliary(iv) Relation of L
reconsider ab = a /\ b as Relation of L ;
 for x being Element of L holds [(Bottom L),x] in ab
proof
let x be Element of L; ::_thesis: [(Bottom L),x] in ab
A1: [(Bottom L),x] in a by Def6;
 [(Bottom L),x] in b by Def6;
hence  [(Bottom L),x] in ab by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  a /\ b is auxiliary(iv) Relation of L by Def6; ::_thesis: verum
end;

theorem Th10: :: WAYBEL_4:10
for L being lower-bounded sup-Semilattice
for a, b being auxiliary Relation of L holds a /\ b is auxiliary Relation of L
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for a, b being auxiliary Relation of L holds a /\ b is auxiliary Relation of L
let a, b be auxiliary Relation of L; ::_thesis: a /\ b is auxiliary Relation of L
reconsider ab = a /\ b as Relation of L ;
 ( ab is auxiliary(i) & ab is auxiliary(ii) & ab is auxiliary(iii) & ab is auxiliary(iv) ) by Th6, Th7, Th8, Th9;
hence  a /\ b is auxiliary Relation of L ; ::_thesis: verum
end;

theorem Th11: :: WAYBEL_4:11
for L being lower-bounded sup-Semilattice
for X being non empty Subset of (InclPoset (Aux L)) holds meet X is auxiliary Relation of L
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for X being non empty Subset of (InclPoset (Aux L)) holds meet X is auxiliary Relation of L
let X be non empty Subset of (InclPoset (Aux L)); ::_thesis: meet X is auxiliary Relation of L
 X c= the carrier of (InclPoset (Aux L)) ;
then A1: X c= Aux L by YELLOW_1:1;
set a = the Element of X;
 the Element of X in X ;
then  the Element of X is auxiliary Relation of L by A1, Def8;
then reconsider ab = meet X as Relation of L by SETFAM_1:7;
A2: ab is auxiliary(i)
proof
let x, y be Element of L; :: according to WAYBEL_4:def_3 ::_thesis: ( [x,y] in ab implies x <= y )
assume A3: [x,y] in ab ; ::_thesis: x <= y
set V = the Element of X;
A4: the Element of X in X ;
A5: [x,y] in the Element of X by A3, SETFAM_1:def_1;
 the Element of X is auxiliary Relation of L by A1, A4, Def8;
hence  x <= y by A5, Def3; ::_thesis: verum
end;
A6: ab is auxiliary(ii)
proof
let x, y, z, u be Element of L; :: according to WAYBEL_4:def_4 ::_thesis: ( u <= x & [x,y] in ab & y <= z implies [u,z] in ab )
assume that
A7: u <= x and
A8: [x,y] in ab and
A9: y <= z ; ::_thesis: [u,z] in ab
 for Y being set st Y in X holds
[u,z] in Y
proof
let Y be set ; ::_thesis: ( Y in X implies [u,z] in Y )
assume A10: Y in X ; ::_thesis: [u,z] in Y
then A11: Y is auxiliary Relation of L by A1, Def8;
 [x,y] in Y by A8, A10, SETFAM_1:def_1;
hence  [u,z] in Y by A7, A9, A11, Def4; ::_thesis: verum
end;
hence  [u,z] in ab by SETFAM_1:def_1; ::_thesis: verum
end;
A12: ab is auxiliary(iii)
proof
let x, y, z be Element of L; :: according to WAYBEL_4:def_5 ::_thesis: ( [x,z] in ab & [y,z] in ab implies [(x "\/" y),z] in ab )
assume that
A13: [x,z] in ab and
A14: [y,z] in ab ; ::_thesis: [(x "\/" y),z] in ab
 for Y being set st Y in X holds
[(x "\/" y),z] in Y
proof
let Y be set ; ::_thesis: ( Y in X implies [(x "\/" y),z] in Y )
assume A15: Y in X ; ::_thesis: [(x "\/" y),z] in Y
then A16: Y is auxiliary Relation of L by A1, Def8;
A17: [x,z] in Y by A13, A15, SETFAM_1:def_1;
 [y,z] in Y by A14, A15, SETFAM_1:def_1;
hence  [(x "\/" y),z] in Y by A16, A17, Def5; ::_thesis: verum
end;
hence  [(x "\/" y),z] in ab by SETFAM_1:def_1; ::_thesis: verum
end;
 ab is auxiliary(iv)
proof
let x be Element of L; :: according to WAYBEL_4:def_6 ::_thesis: [(Bottom L),x] in ab
 for Y being set st Y in X holds
[(Bottom L),x] in Y
proof
let Y be set ; ::_thesis: ( Y in X implies [(Bottom L),x] in Y )
assume  Y in X ; ::_thesis: [(Bottom L),x] in Y
then  Y is auxiliary Relation of L by A1, Def8;
hence  [(Bottom L),x] in Y by Def6; ::_thesis: verum
end;
hence  [(Bottom L),x] in ab by SETFAM_1:def_1; ::_thesis: verum
end;
hence  meet X is auxiliary Relation of L by A2, A6, A12; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
cluster InclPoset (Aux L) ->  with_infima ;
coherence
 InclPoset (Aux L) is with_infima
proof
 for x, y being set st x in Aux L & y in Aux L holds
x /\ y in Aux L
proof
let x, y be set ; ::_thesis: ( x in Aux L & y in Aux L implies x /\ y in Aux L )
assume that
A1: x in Aux L and
A2: y in Aux L ; ::_thesis: x /\ y in Aux L
A3: x is auxiliary Relation of L by A1, Def8;
 y is auxiliary Relation of L by A2, Def8;
then  x /\ y is auxiliary Relation of L by A3, Th10;
hence  x /\ y in Aux L by Def8; ::_thesis: verum
end;
hence  InclPoset (Aux L) is with_infima by YELLOW_1:12; ::_thesis: verum
end;
end;

registration
let L be lower-bounded sup-Semilattice;
cluster InclPoset (Aux L) ->  complete ;
coherence
 InclPoset (Aux L) is complete
proof
 for X being Subset of (InclPoset (Aux L)) holds ex_inf_of X, InclPoset (Aux L)
proof
let X be Subset of (InclPoset (Aux L)); ::_thesis: ex_inf_of X, InclPoset (Aux L)
set N = meet X;
percases ( X <> {} or X = {} ) ;
supposeA1: X <> {} ; ::_thesis: ex_inf_of X, InclPoset (Aux L)
then  meet X is auxiliary Relation of L by Th11;
then  meet X in Aux L by Def8;
then reconsider N = meet X as Element of (InclPoset (Aux L)) by YELLOW_1:1;
A2: X is_>=_than N
proof
let b be Element of (InclPoset (Aux L)); :: according to LATTICE3:def_8 ::_thesis: ( not b in X or N <= b )
assume  b in X ; ::_thesis: N <= b
then  N c= b by SETFAM_1:3;
hence  N <= b by YELLOW_1:3; ::_thesis: verum
end;
 for b being Element of (InclPoset (Aux L)) st X is_>=_than b holds
N >= b
proof
let b be Element of (InclPoset (Aux L)); ::_thesis: ( X is_>=_than b implies N >= b )
assume A3: X is_>=_than b ; ::_thesis: N >= b
 for Z1 being set st Z1 in X holds
b c= Z1
proof
let Z1 be set ; ::_thesis: ( Z1 in X implies b c= Z1 )
assume A4: Z1 in X ; ::_thesis: b c= Z1
then reconsider Z19 = Z1 as Element of (InclPoset (Aux L)) ;
 b <= Z19 by A3, A4, LATTICE3:def_8;
hence  b c= Z1 by YELLOW_1:3; ::_thesis: verum
end;
then  b c= meet X by A1, SETFAM_1:5;
hence  N >= b by YELLOW_1:3; ::_thesis: verum
end;
hence  ex_inf_of X, InclPoset (Aux L) by A2, YELLOW_0:16; ::_thesis: verum
end;
suppose X = {} ; ::_thesis: ex_inf_of X, InclPoset (Aux L)
hence  ex_inf_of X, InclPoset (Aux L) by YELLOW_0:43; ::_thesis: verum
end;
end;
end;
hence  InclPoset (Aux L) is complete by YELLOW_2:28; ::_thesis: verum
end;
end;

definition
let L be non empty RelStr ;
let x be Element of L;
let AR be Relation of the carrier of L;
A1:  {  y where y is Element of L : [y,x] in AR  }  c= the carrier of L
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  y where y is Element of L : [y,x] in AR  }  or z in the carrier of L )
assume  z in  {  y where y is Element of L : [y,x] in AR  }  ; ::_thesis: z in the carrier of L
then  ex y being Element of L st
( z = y & [y,x] in AR ) ;
hence  z in the carrier of L ; ::_thesis: verum
end;
funcAR -below x ->  Subset of L equals :: WAYBEL_4:def 10
 {  y where y is Element of L : [y,x] in AR  }  ;
correctness
coherence
{  y where y is Element of L : [y,x] in AR  }  is Subset of L;
by A1;
A2:  {  y where y is Element of L : [x,y] in AR  }  c= the carrier of L
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  y where y is Element of L : [x,y] in AR  }  or z in the carrier of L )
assume  z in  {  y where y is Element of L : [x,y] in AR  }  ; ::_thesis: z in the carrier of L
then  ex y being Element of L st
( z = y & [x,y] in AR ) ;
hence  z in the carrier of L ; ::_thesis: verum
end;
funcAR -above x ->  Subset of L equals :: WAYBEL_4:def 11
 {  y where y is Element of L : [x,y] in AR  }  ;
correctness
coherence
{  y where y is Element of L : [x,y] in AR  }  is Subset of L;
by A2;
end;

:: deftheorem  defines -below WAYBEL_4:def_10_:_
 for L being non empty RelStr
for x being Element of L
for AR being Relation of the carrier of L holds AR -below x =  {  y where y is Element of L : [y,x] in AR  }  ;

:: deftheorem  defines -above WAYBEL_4:def_11_:_
 for L being non empty RelStr
for x being Element of L
for AR being Relation of the carrier of L holds AR -above x =  {  y where y is Element of L : [x,y] in AR  }  ;

theorem Th12: :: WAYBEL_4:12
for L being lower-bounded sup-Semilattice
for x being Element of L
for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for x being Element of L
for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x
let x be Element of L; ::_thesis: for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x
let AR be auxiliary(i) Relation of L; ::_thesis: AR -below x c= downarrow x
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in AR -below x or a in downarrow x )
assume  a in AR -below x ; ::_thesis: a in downarrow x
then consider y1 being Element of L such that
A1: y1 = a and
A2: [y1,x] in AR ;
 y1 <= x by A2, Def3;
hence  a in downarrow x by A1, WAYBEL_0:17; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
let x be Element of L;
let AR be auxiliary(iv) Relation of L;
clusterAR -below x ->  non empty ;
coherence
 not AR -below x is empty
proof
set I = AR -below x;
 [(Bottom L),x] in AR by Def6;
then  Bottom L in AR -below x ;
hence  not AR -below x is empty ; ::_thesis: verum
end;
end;

registration
let L be lower-bounded sup-Semilattice;
let x be Element of L;
let AR be auxiliary(ii) Relation of L;
clusterAR -below x ->  lower ;
coherence
 AR -below x is lower
proof
set I = AR -below x;
let x1, y1 be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( not x1 in AR -below x or not y1 <= x1 or y1 in AR -below x )
assume that
A1: x1 in AR -below x and
A2: y1 <= x1 ; ::_thesis: y1 in AR -below x
A3: ex v1 being Element of L st
( v1 = x1 & [v1,x] in AR ) by A1;
 x <= x ;
then  [y1,x] in AR by A2, A3, Def4;
hence  y1 in AR -below x ; ::_thesis: verum
end;
end;

registration
let L be lower-bounded sup-Semilattice;
let x be Element of L;
let AR be auxiliary(iii) Relation of L;
clusterAR -below x ->  directed ;
coherence
 AR -below x is directed
proof
set I = AR -below x;
let u1, u2 be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not u1 in AR -below x or not u2 in AR -below x or ex b1 being Element of the carrier of L st
( b1 in AR -below x & u1 <= b1 & u2 <= b1 ) )
assume that
A1: u1 in AR -below x and
A2: u2 in AR -below x ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in AR -below x & u1 <= b1 & u2 <= b1 )
A3: ex v1 being Element of L st
( v1 = u1 & [v1,x] in AR ) by A1;
A4: ex v2 being Element of L st
( v2 = u2 & [v2,x] in AR ) by A2;
take u12 = u1 "\/" u2; ::_thesis: ( u12 in AR -below x & u1 <= u12 & u2 <= u12 )
 [u12,x] in AR by A3, A4, Def5;
hence  ( u12 in AR -below x & u1 <= u12 & u2 <= u12 ) by YELLOW_0:22; ::_thesis: verum
end;
end;

definition
let L be lower-bounded sup-Semilattice;
let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;
funcAR -below  ->  Function of L,(InclPoset (Ids L)) means :Def12: :: WAYBEL_4:def 12
 for x being Element of L holds it . x = AR -below x;
existence
 ex b1 being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds b1 . x = AR -below x
proof
deffunc H1( Element of L) ->  Subset of L = AR -below $1;
A1: for x being Element of L holds H1(x) is Element of (InclPoset (Ids L))
proof
let x be Element of L; ::_thesis: H1(x) is Element of (InclPoset (Ids L))
reconsider I = H1(x) as Ideal of L ;
 I in Ids L ;
hence  H1(x) is Element of (InclPoset (Ids L)) by YELLOW_1:1; ::_thesis: verum
end;
consider f being Function of L,(InclPoset (Ids L)) such that
A2: for x being Element of L holds f . x = H1(x) from FUNCT_2:sch_9(A1);
take  f ; ::_thesis: for x being Element of L holds f . x = AR -below x
thus  for x being Element of L holds f . x = AR -below x by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b1 . x = AR -below x ) & ( for x being Element of L holds b2 . x = AR -below x ) holds
b1 = b2
proof
let M1, M2 be Function of L,(InclPoset (Ids L)); ::_thesis: ( ( for x being Element of L holds M1 . x = AR -below x ) & ( for x being Element of L holds M2 . x = AR -below x ) implies M1 = M2 )
assume A3: for x being Element of L holds M1 . x = AR -below x ; ::_thesis: ( ex x being Element of L st not M2 . x = AR -below x or M1 = M2 )
assume A4: for x being Element of L holds M2 . x = AR -below x ; ::_thesis: M1 = M2
 for x being set st x in the carrier of L holds
M1 . x = M2 . x
proof
let x be set ; ::_thesis: ( x in the carrier of L implies M1 . x = M2 . x )
assume  x in the carrier of L ; ::_thesis: M1 . x = M2 . x
then reconsider x9 = x as Element of L ;
thus M1 . x = AR -below x9 by A3
.= M2 . x by A4 ; ::_thesis: verum
end;
hence  M1 = M2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines -below WAYBEL_4:def_12_:_
 for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L
for b3 being Function of L,(InclPoset (Ids L)) holds
( b3 = AR -below iff for x being Element of L holds b3 . x = AR -below x );

theorem Th13: :: WAYBEL_4:13
for L being non empty RelStr
for AR being Relation of L
for a being set
for y being Element of L holds
( a in AR -below y iff [a,y] in AR )
proof
let L be non empty RelStr ; ::_thesis: for AR being Relation of L
for a being set
for y being Element of L holds
( a in AR -below y iff [a,y] in AR )
let AR be Relation of L; ::_thesis: for a being set
for y being Element of L holds
( a in AR -below y iff [a,y] in AR )
let a be set ; ::_thesis: for y being Element of L holds
( a in AR -below y iff [a,y] in AR )
let y be Element of L; ::_thesis: ( a in AR -below y iff [a,y] in AR )
 ( a in AR -below y iff [a,y] in AR )
proof
hereby  ::_thesis: ( [a,y] in AR implies a in AR -below y )
assume  a in AR -below y ; ::_thesis: [a,y] in AR
then  ex z being Element of L st
( a = z & [z,y] in AR ) ;
hence  [a,y] in AR ; ::_thesis: verum
end;
assume A1: [a,y] in AR ; ::_thesis: a in AR -below y
then reconsider x9 = a as Element of L by ZFMISC_1:87;
 ex z being Element of L st
( a = z & [z,y] in AR )
proof
take  x9 ; ::_thesis: ( a = x9 & [x9,y] in AR )
thus  ( a = x9 & [x9,y] in AR ) by A1; ::_thesis: verum
end;
hence  a in AR -below y ; ::_thesis: verum
end;
hence  ( a in AR -below y iff [a,y] in AR ) ; ::_thesis: verum
end;

theorem :: WAYBEL_4:14
for a being set
for L being sup-Semilattice
for AR being Relation of L
for y being Element of L holds
( a in AR -above y iff [y,a] in AR )
proof
let a be set ; ::_thesis: for L being sup-Semilattice
for AR being Relation of L
for y being Element of L holds
( a in AR -above y iff [y,a] in AR )
let L be with_suprema Poset; ::_thesis: for AR being Relation of L
for y being Element of L holds
( a in AR -above y iff [y,a] in AR )
let AR be Relation of L; ::_thesis: for y being Element of L holds
( a in AR -above y iff [y,a] in AR )
let y be Element of L; ::_thesis: ( a in AR -above y iff [y,a] in AR )
 ( a in AR -above y iff [y,a] in AR )
proof
hereby  ::_thesis: ( [y,a] in AR implies a in AR -above y )
assume  a in AR -above y ; ::_thesis: [y,a] in AR
then  ex z being Element of L st
( a = z & [y,z] in AR ) ;
hence  [y,a] in AR ; ::_thesis: verum
end;
assume A1: [y,a] in AR ; ::_thesis: a in AR -above y
then reconsider x9 = a as Element of L by ZFMISC_1:87;
 ex z being Element of L st
( a = z & [y,z] in AR )
proof
take  x9 ; ::_thesis: ( a = x9 & [y,x9] in AR )
thus  ( a = x9 & [y,x9] in AR ) by A1; ::_thesis: verum
end;
hence  a in AR -above y ; ::_thesis: verum
end;
hence  ( a in AR -above y iff [y,a] in AR ) ; ::_thesis: verum
end;

Lm3:  for L being lower-bounded with_suprema Poset
for AR being Relation of L
for a being set
for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for AR being Relation of L
for a being set
for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )
let AR be Relation of L; ::_thesis: for a being set
for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )
let a be set ; ::_thesis: for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )
let y be Element of L; ::_thesis: ( a in downarrow y iff [a,y] in the InternalRel of L )
hereby  ::_thesis: ( [a,y] in the InternalRel of L implies a in downarrow y )
assume A1: a in downarrow y ; ::_thesis: [a,y] in the InternalRel of L
then reconsider a9 = a as Element of L ;
 a9 <= y by A1, WAYBEL_0:17;
hence  [a,y] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
assume A2: [a,y] in the InternalRel of L ; ::_thesis: a in downarrow y
then reconsider a9 = a as Element of L by ZFMISC_1:87;
 a9 <= y by A2, ORDERS_2:def_5;
hence  a in downarrow y by WAYBEL_0:17; ::_thesis: verum
end;

theorem :: WAYBEL_4:15
for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L
for x being Element of L st AR = the InternalRel of L holds
AR -below x = downarrow x
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary(i) Relation of L
for x being Element of L st AR = the InternalRel of L holds
AR -below x = downarrow x
let AR be auxiliary(i) Relation of L; ::_thesis: for x being Element of L st AR = the InternalRel of L holds
AR -below x = downarrow x
let x be Element of L; ::_thesis: ( AR = the InternalRel of L implies AR -below x = downarrow x )
assume A1: AR = the InternalRel of L ; ::_thesis: AR -below x = downarrow x
thus  AR -below x c= downarrow x by Th12; :: according to XBOOLE_0:def_10 ::_thesis: downarrow x c= AR -below x
thus  downarrow x c= AR -below x ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in AR -below x )
assume  a in downarrow x ; ::_thesis: a in AR -below x
then  [a,x] in AR by A1, Lm3;
hence  a in AR -below x by Th13; ::_thesis: verum
end;
end;

definition
let L be non empty Poset;
func MonSet L ->  strict RelStr  means :Def13: :: WAYBEL_4:def 13
 for a being set holds
( ( a in the carrier of it implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of it ) & ( for c, d being set holds
( [c,d] in the InternalRel of it iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of it & d in the carrier of it & f <= g ) ) ) );
existence
 ex b1 being strict RelStr st
for a being set holds
( ( a in the carrier of b1 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b1 ) & ( for c, d being set holds
( [c,d] in the InternalRel of b1 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b1 & d in the carrier of b1 & f <= g ) ) ) )
proof
defpred S1[ set ] means  ex s being Function of L,(InclPoset (Ids L)) st
( $1 = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) );
consider S being set  such that
A1: for a being set holds
( a in S iff ( a in PFuncs ( the carrier of L, the carrier of (InclPoset (Ids L))) & S1[a] ) ) from XBOOLE_0:sch_1();
A2: for a being set holds
( a in S iff ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) )
proof
let a be set ; ::_thesis: ( a in S iff ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) )
thus  ( a in S implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) by A1; ::_thesis: ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in S )
given s being Function of L,(InclPoset (Ids L)) such that A3: a = s and
A4: s is monotone and
A5: for x being Element of L holds s . x c= downarrow x ; ::_thesis: a in S
 s in PFuncs ( the carrier of L, the carrier of (InclPoset (Ids L))) by PARTFUN1:45;
hence  a in S by A1, A3, A4, A5; ::_thesis: verum
end;
defpred S2[ set , set ] means  ex f, g being Function of L,(InclPoset (Ids L)) st
( $1 = f & $2 = g & f <= g );
consider R being Relation of S,S such that
A6: for c, d being set holds
( [c,d] in R iff ( c in S & d in S & S2[c,d] ) ) from RELSET_1:sch_1();
A7: for c, d being set holds
( [c,d] in R iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) )
proof
let c, d be set ; ::_thesis: ( [c,d] in R iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) )
hereby  ::_thesis: ( ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) implies [c,d] in R )
assume A8: [c,d] in R ; ::_thesis: ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g )
then A9: c in S by A6;
A10: d in S by A6, A8;
 ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & f <= g ) by A6, A8;
hence  ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in S & d in S & f <= g ) by A9, A10; ::_thesis: verum
end;
given f, g being Function of L,(InclPoset (Ids L)) such that A11: c = f and
A12: d = g and
A13: c in S and
A14: d in S and
A15: f <= g ; ::_thesis: [c,d] in R
thus  [c,d] in R by A6, A11, A12, A13, A14, A15; ::_thesis: verum
end;
take  RelStr(# S,R #) ; ::_thesis: for a being set holds
( ( a in the carrier of RelStr(# S,R #) implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of RelStr(# S,R #) ) & ( for c, d being set holds
( [c,d] in the InternalRel of RelStr(# S,R #) iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of RelStr(# S,R #) & d in the carrier of RelStr(# S,R #) & f <= g ) ) ) )
thus  for a being set holds
( ( a in the carrier of RelStr(# S,R #) implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of RelStr(# S,R #) ) & ( for c, d being set holds
( [c,d] in the InternalRel of RelStr(# S,R #) iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of RelStr(# S,R #) & d in the carrier of RelStr(# S,R #) & f <= g ) ) ) ) by A2, A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict RelStr st ( for a being set holds
( ( a in the carrier of b1 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b1 ) & ( for c, d being set holds
( [c,d] in the InternalRel of b1 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b1 & d in the carrier of b1 & f <= g ) ) ) ) ) & ( for a being set holds
( ( a in the carrier of b2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b2 ) & ( for c, d being set holds
( [c,d] in the InternalRel of b2 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b2 & d in the carrier of b2 & f <= g ) ) ) ) ) holds
b1 = b2
proof
let R1, R2 be strict RelStr ; ::_thesis: ( ( for a being set holds
( ( a in the carrier of R1 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R1 ) & ( for c, d being set holds
( [c,d] in the InternalRel of R1 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R1 & d in the carrier of R1 & f <= g ) ) ) ) ) & ( for a being set holds
( ( a in the carrier of R2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R2 ) & ( for c, d being set holds
( [c,d] in the InternalRel of R2 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) ) ) ) ) implies R1 = R2 )
assume A16: for a being set holds
( ( a in the carrier of R1 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R1 ) & ( for c, d being set holds
( [c,d] in the InternalRel of R1 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R1 & d in the carrier of R1 & f <= g ) ) ) ) ; ::_thesis: ( ex a being set st
( ( a in the carrier of R2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R2 ) implies ex c, d being set st
( ( [c,d] in the InternalRel of R2 implies ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) ) implies ( ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) & not [c,d] in the InternalRel of R2 ) ) ) or R1 = R2 )
assume A17: for a being set holds
( ( a in the carrier of R2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R2 ) & ( for c, d being set holds
( [c,d] in the InternalRel of R2 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) ) ) ) ; ::_thesis: R1 = R2
A18: the carrier of R1 c= the carrier of R2
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in the carrier of R1 or b in the carrier of R2 )
assume  b in the carrier of R1 ; ::_thesis: b in the carrier of R2
then  ex s being Function of L,(InclPoset (Ids L)) st
( b = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by A16;
hence  b in the carrier of R2 by A17; ::_thesis: verum
end;
A19: the carrier of R2 c= the carrier of R1
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in the carrier of R2 or b in the carrier of R1 )
assume  b in the carrier of R2 ; ::_thesis: b in the carrier of R1
then  ex s being Function of L,(InclPoset (Ids L)) st
( b = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by A17;
hence  b in the carrier of R1 by A16; ::_thesis: verum
end;
 the InternalRel of R1 = the InternalRel of R2
proof
let c, d be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [c,d] in the InternalRel of R1 or [c,d] in the InternalRel of R2 ) & ( not [c,d] in the InternalRel of R2 or [c,d] in the InternalRel of R1 ) )
A20: now__::_thesis:_(_[c,d]_in_the_InternalRel_of_R1_implies_[c,d]_in_the_InternalRel_of_R2_)
assume  [c,d] in the InternalRel of R1 ; ::_thesis: [c,d] in the InternalRel of R2
then  ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R1 & d in the carrier of R1 & f <= g ) by A16;
hence  [c,d] in the InternalRel of R2 by A17, A18; ::_thesis: verum
end;
now__::_thesis:_(_[c,d]_in_the_InternalRel_of_R2_implies_[c,d]_in_the_InternalRel_of_R1_)
assume  [c,d] in the InternalRel of R2 ; ::_thesis: [c,d] in the InternalRel of R1
then  ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) by A17;
hence  [c,d] in the InternalRel of R1 by A16, A19; ::_thesis: verum
end;
hence  ( ( not [c,d] in the InternalRel of R1 or [c,d] in the InternalRel of R2 ) & ( not [c,d] in the InternalRel of R2 or [c,d] in the InternalRel of R1 ) ) by A20; ::_thesis: verum
end;
hence  R1 = R2 by A18, A19, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines MonSet WAYBEL_4:def_13_:_
 for L being non empty Poset
for b2 being strict RelStr holds
( b2 = MonSet L iff for a being set holds
( ( a in the carrier of b2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b2 ) & ( for c, d being set holds
( [c,d] in the InternalRel of b2 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b2 & d in the carrier of b2 & f <= g ) ) ) ) );

theorem :: WAYBEL_4:16
for L being lower-bounded sup-Semilattice holds MonSet L is full SubRelStr of (InclPoset (Ids L)) |^ the carrier of L
proof
let L be lower-bounded sup-Semilattice; ::_thesis: MonSet L is full SubRelStr of (InclPoset (Ids L)) |^ the carrier of L
set J = the carrier of L --> (InclPoset (Ids L));
A1: the carrier of (MonSet L) c= the carrier of ((InclPoset (Ids L)) |^ the carrier of L)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of (MonSet L) or a in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) )
assume  a in the carrier of (MonSet L) ; ::_thesis: a in the carrier of ((InclPoset (Ids L)) |^ the carrier of L)
then consider s being Function of L,(InclPoset (Ids L)) such that
A2: a = s and
 s is monotone and
 for x being Element of L holds s . x c= downarrow x by Def13;
 s in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by FUNCT_2:8;
hence  a in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) by A2, YELLOW_1:28; ::_thesis: verum
end;
A3: the InternalRel of (MonSet L) c= the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L)
proof
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in the InternalRel of (MonSet L) or [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) )
assume  [a,b] in the InternalRel of (MonSet L) ; ::_thesis: [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L)
then consider f, g being Function of L,(InclPoset (Ids L)) such that
A4: a = f and
A5: b = g and
 a in the carrier of (MonSet L) and
 b in the carrier of (MonSet L) and
A6: f <= g by Def13;
set AG = product ( the carrier of L --> (InclPoset (Ids L)));
A7: product ( the carrier of L --> (InclPoset (Ids L))) = (InclPoset (Ids L)) |^ the carrier of L by YELLOW_1:def_5;
A8: f in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by FUNCT_2:8;
A9: g in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by FUNCT_2:8;
A10: f in the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))) by A7, A8, YELLOW_1:28;
reconsider f9 = f, g9 = g as Element of (product ( the carrier of L --> (InclPoset (Ids L)))) by A7, A8, A9, YELLOW_1:28;
A11: f9 in product (Carrier ( the carrier of L --> (InclPoset (Ids L)))) by A10, YELLOW_1:def_4;
 ex ff, gg being Function st
( ff = f9 & gg = g9 & ( for i being set st i in the carrier of L holds
ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = ff . i & yi = gg . i & xi <= yi ) ) )
proof
take  f ; ::_thesis: ex gg being Function st
( f = f9 & gg = g9 & ( for i being set st i in the carrier of L holds
ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = gg . i & xi <= yi ) ) )
take  g ; ::_thesis: ( f = f9 & g = g9 & ( for i being set st i in the carrier of L holds
ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
thus  ( f = f9 & g = g9 ) ; ::_thesis: for i being set st i in the carrier of L holds
ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi )
let i be set ; ::_thesis: ( i in the carrier of L implies ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi ) )
assume A12: i in the carrier of L ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi )
then reconsider i9 = i as Element of L ;
take R = InclPoset (Ids L); ::_thesis: ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi )
reconsider xi = f . i9, yi = g . i9 as Element of R ;
take  xi ; ::_thesis: ex yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi )
take  yi ; ::_thesis: ( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi )
thus  ( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i ) by A12, FUNCOP_1:7; ::_thesis: xi <= yi
reconsider i9 = i as Element of L by A12;
 ex a, b being Element of (InclPoset (Ids L)) st
( a = f . i9 & b = g . i9 & a <= b ) by A6, YELLOW_2:def_1;
hence  xi <= yi ; ::_thesis: verum
end;
then  f9 <= g9 by A11, YELLOW_1:def_4;
then  [a,b] in the InternalRel of (product ( the carrier of L --> (InclPoset (Ids L)))) by A4, A5, ORDERS_2:def_5;
hence  [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) by YELLOW_1:def_5; ::_thesis: verum
end;
set J = the carrier of L --> (InclPoset (Ids L));
 the InternalRel of (MonSet L) = the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L)
proof
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of (MonSet L) or [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L) ) & ( not [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L) or [a,b] in the InternalRel of (MonSet L) ) )
thus  ( [a,b] in the InternalRel of (MonSet L) implies [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L) ) by A3, XBOOLE_0:def_4; ::_thesis: ( not [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L) or [a,b] in the InternalRel of (MonSet L) )
assume A13: [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L) ; ::_thesis: [a,b] in the InternalRel of (MonSet L)
then A14: [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) by XBOOLE_0:def_4;
A15: [a,b] in [: the carrier of (MonSet L), the carrier of (MonSet L):] by A13, XBOOLE_0:def_4;
A16: a in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) by A14, ZFMISC_1:87;
A17: b in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) by A14, ZFMISC_1:87;
A18: a in the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))) by A16, YELLOW_1:def_5;
reconsider a9 = a, b9 = b as Element of (product ( the carrier of L --> (InclPoset (Ids L)))) by A16, A17, YELLOW_1:def_5;
 [a9,b9] in the InternalRel of (product ( the carrier of L --> (InclPoset (Ids L)))) by A14, YELLOW_1:def_5;
then A19: a9 <= b9 by ORDERS_2:def_5;
 a9 in product (Carrier ( the carrier of L --> (InclPoset (Ids L)))) by A18, YELLOW_1:def_4;
then consider f, g being Function such that
A20: f = a9 and
A21: g = b9 and
A22: for i being set st i in the carrier of L holds
ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi ) by A19, YELLOW_1:def_4;
A23: f in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by A16, A20, YELLOW_1:28;
 g in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by A17, A21, YELLOW_1:28;
then reconsider f = f, g = g as Function of the carrier of L, the carrier of (InclPoset (Ids L)) by A23, FUNCT_2:66;
reconsider f = f, g = g as Function of L,(InclPoset (Ids L)) ;
now__::_thesis:_ex_f,_g_being_Function_of_L,(InclPoset_(Ids_L))_st_
(_a9_=_f_&_b9_=_g_&_a9_in_the_carrier_of_(MonSet_L)_&_b9_in_the_carrier_of_(MonSet_L)_&_f_<=_g_)
take f = f; ::_thesis: ex g being Function of L,(InclPoset (Ids L)) st
( a9 = f & b9 = g & a9 in the carrier of (MonSet L) & b9 in the carrier of (MonSet L) & f <= g )
take g = g; ::_thesis: ( a9 = f & b9 = g & a9 in the carrier of (MonSet L) & b9 in the carrier of (MonSet L) & f <= g )
 f <= g
proof
let j be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not j in the carrier of L or ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = f . j & b2 = g . j & b1 <= b2 ) )
assume  j in the carrier of L ; ::_thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = f . j & b2 = g . j & b1 <= b2 )
then reconsider j9 = j as Element of L ;
take  f . j9 ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Ids L)) st
( f . j9 = f . j & b1 = g . j & f . j9 <= b1 )
take  g . j9 ; ::_thesis: ( f . j9 = f . j & g . j9 = g . j & f . j9 <= g . j9 )
 ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . j9 & xi = f . j9 & yi = g . j9 & xi <= yi ) by A22;
hence  ( f . j9 = f . j & g . j9 = g . j & f . j9 <= g . j9 ) by FUNCOP_1:7; ::_thesis: verum
end;
hence  ( a9 = f & b9 = g & a9 in the carrier of (MonSet L) & b9 in the carrier of (MonSet L) & f <= g ) by A15, A20, A21, ZFMISC_1:87; ::_thesis: verum
end;
hence  [a,b] in the InternalRel of (MonSet L) by Def13; ::_thesis: verum
end;
hence  MonSet L is full SubRelStr of (InclPoset (Ids L)) |^ the carrier of L by A1, A3, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum
end;

theorem Th17: :: WAYBEL_4:17
for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) Relation of L
for x, y being Element of L st x <= y holds
AR -below x c= AR -below y
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary(ii) Relation of L
for x, y being Element of L st x <= y holds
AR -below x c= AR -below y
let AR be auxiliary(ii) Relation of L; ::_thesis: for x, y being Element of L st x <= y holds
AR -below x c= AR -below y
let x, y be Element of L; ::_thesis: ( x <= y implies AR -below x c= AR -below y )
assume A1: x <= y ; ::_thesis: AR -below x c= AR -below y
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in AR -below x or a in AR -below y )
assume  a in AR -below x ; ::_thesis: a in AR -below y
then consider y2 being Element of L such that
A2: y2 = a and
A3: [y2,x] in AR ;
 y2 <= y2 ;
then  [y2,y] in AR by A1, A3, Def4;
hence  a in AR -below y by A2; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;
clusterAR -below  ->  monotone ;
coherence
 AR -below is monotone
proof
set s = AR -below ;
let x, y be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (AR -below) . x or not b2 = (AR -below) . y or b1 <= b2 ) )
A1: (AR -below) . x = AR -below x by Def12;
A2: (AR -below) . y = AR -below y by Def12;
assume  x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (AR -below) . x or not b2 = (AR -below) . y or b1 <= b2 )
then  AR -below x c= AR -below y by Th17;
hence  for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (AR -below) . x or not b2 = (AR -below) . y or b1 <= b2 ) by A1, A2, YELLOW_1:3; ::_thesis: verum
end;
end;

theorem Th18: :: WAYBEL_4:18
for L being lower-bounded sup-Semilattice
for AR being auxiliary Relation of L holds AR -below in the carrier of (MonSet L)
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary Relation of L holds AR -below in the carrier of (MonSet L)
let AR be auxiliary Relation of L; ::_thesis: AR -below in the carrier of (MonSet L)
set s = AR -below ;
 ex s being Function of L,(InclPoset (Ids L)) st
( AR -below = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) )
proof
take  AR -below ; ::_thesis: ( AR -below = AR -below & AR -below is monotone & ( for x being Element of L holds (AR -below) . x c= downarrow x ) )
 for x being Element of L holds (AR -below) . x c= downarrow x
proof
let x be Element of L; ::_thesis: (AR -below) . x c= downarrow x
 (AR -below) . x = AR -below x by Def12;
hence  (AR -below) . x c= downarrow x by Th12; ::_thesis: verum
end;
hence  ( AR -below = AR -below & AR -below is monotone & ( for x being Element of L holds (AR -below) . x c= downarrow x ) ) ; ::_thesis: verum
end;
hence  AR -below in the carrier of (MonSet L) by Def13; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
cluster MonSet L ->  non empty strict ;
coherence
 not MonSet L is empty by Th18;
end;

theorem Th19: :: WAYBEL_4:19
for L being lower-bounded sup-Semilattice holds IdsMap L in the carrier of (MonSet L)
proof
let L be lower-bounded sup-Semilattice; ::_thesis: IdsMap L in the carrier of (MonSet L)
set s = IdsMap L;
 ex s9 being Function of L,(InclPoset (Ids L)) st
( IdsMap L = s9 & s9 is monotone & ( for x being Element of L holds s9 . x c= downarrow x ) )
proof
take  IdsMap L ; ::_thesis: ( IdsMap L = IdsMap L & IdsMap L is monotone & ( for x being Element of L holds (IdsMap L) . x c= downarrow x ) )
thus  ( IdsMap L = IdsMap L & IdsMap L is monotone & ( for x being Element of L holds (IdsMap L) . x c= downarrow x ) ) by YELLOW_2:def_4; ::_thesis: verum
end;
hence  IdsMap L in the carrier of (MonSet L) by Def13; ::_thesis: verum
end;

theorem :: WAYBEL_4:20
for L being lower-bounded sup-Semilattice
for AR being auxiliary Relation of L holds AR -below <= IdsMap L
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary Relation of L holds AR -below <= IdsMap L
let AR be auxiliary Relation of L; ::_thesis: AR -below <= IdsMap L
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 (InclPoset (Ids L)) st
( b1 = (AR -below) . x & b2 = (IdsMap L) . x & b1 <= b2 ) )
assume  x in the carrier of L ; ::_thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = (AR -below) . x & b2 = (IdsMap L) . x & b1 <= b2 )
then reconsider x9 = x as Element of L ;
A1: (AR -below) . x9 = AR -below x9 by Def12;
 (IdsMap L) . x9 = downarrow x9 by YELLOW_2:def_4;
then A2: (AR -below) . x c= (IdsMap L) . x by A1, Th12;
reconsider a = (AR -below) . x9, b = (IdsMap L) . x9 as Element of (InclPoset (Ids L)) ;
take  a ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Ids L)) st
( a = (AR -below) . x & b1 = (IdsMap L) . x & a <= b1 )
take  b ; ::_thesis: ( a = (AR -below) . x & b = (IdsMap L) . x & a <= b )
thus  ( a = (AR -below) . x & b = (IdsMap L) . x & a <= b ) by A2, YELLOW_1:3; ::_thesis: verum
end;

theorem Th21: :: WAYBEL_4:21
for L being non empty lower-bounded Poset
for I being Ideal of L holds Bottom L in I
proof
let L be non empty lower-bounded Poset; ::_thesis: for I being Ideal of L holds Bottom L in I
let I be Ideal of L; ::_thesis: Bottom L in I
set x = the Element of I;
 Bottom L <= the Element of I by YELLOW_0:44;
hence  Bottom L in I by WAYBEL_0:def_19; ::_thesis: verum
end;

theorem :: WAYBEL_4:22
for L being non empty upper-bounded Poset
for F being Filter of L holds Top L in F
proof
let L be non empty upper-bounded Poset; ::_thesis: for F being Filter of L holds Top L in F
let F be Filter of L; ::_thesis: Top L in F
set x = the Element of F;
 Top L >= the Element of F by YELLOW_0:45;
hence  Top L in F by WAYBEL_0:def_20; ::_thesis: verum
end;

theorem Th23: :: WAYBEL_4:23
for L being non empty lower-bounded Poset holds downarrow (Bottom L) = {(Bottom L)}
proof
let L be non empty lower-bounded Poset; ::_thesis: downarrow (Bottom L) = {(Bottom L)}
thus  downarrow (Bottom L) c= {(Bottom L)} :: according to XBOOLE_0:def_10 ::_thesis: {(Bottom L)} c= downarrow (Bottom L)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow (Bottom L) or a in {(Bottom L)} )
assume  a in downarrow (Bottom L) ; ::_thesis: a in {(Bottom L)}
then  a in  {  x where x is Element of L : ex y being Element of L st
( x <= y & y in {(Bottom L)} )  }  by WAYBEL_0:14;
then consider a9 being Element of L such that
A1: a9 = a and
A2: ex y being Element of L st
( a9 <= y & y in {(Bottom L)} ) ;
consider y being Element of L such that
A3: a9 <= y and
A4: y in {(Bottom L)} by A2;
A5: Bottom L <= a9 by YELLOW_0:44;
 y = Bottom L by A4, TARSKI:def_1;
hence  a in {(Bottom L)} by A1, A3, A4, A5, ORDERS_2:2; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(Bottom L)} or a in downarrow (Bottom L) )
assume  a in {(Bottom L)} ; ::_thesis: a in downarrow (Bottom L)
then A6: a = Bottom L by TARSKI:def_1;
 Bottom L <= Bottom L ;
hence  a in downarrow (Bottom L) by A6, WAYBEL_0:17; ::_thesis: verum
end;

theorem :: WAYBEL_4:24
for L being non empty upper-bounded Poset holds uparrow (Top L) = {(Top L)}
proof
let L be non empty upper-bounded Poset; ::_thesis: uparrow (Top L) = {(Top L)}
thus  uparrow (Top L) c= {(Top L)} :: according to XBOOLE_0:def_10 ::_thesis: {(Top L)} c= uparrow (Top L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow (Top L) or x in {(Top L)} )
assume A1: x in uparrow (Top L) ; ::_thesis: x in {(Top L)}
then reconsider x = x as Element of L ;
A2: x >= Top L by A1, WAYBEL_0:18;
 x <= Top L by YELLOW_0:45;
then  x = Top L by A2, ORDERS_2:2;
hence  x in {(Top L)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Top L)} or x in uparrow (Top L) )
assume  x in {(Top L)} ; ::_thesis: x in uparrow (Top L)
then A3: x = Top L by TARSKI:def_1;
 Top L <= Top L ;
hence  x in uparrow (Top L) by A3, WAYBEL_0:18; ::_thesis: verum
end;

Lm4:  for L being lower-bounded sup-Semilattice
for I being Ideal of L holds {(Bottom L)} c= I
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for I being Ideal of L holds {(Bottom L)} c= I
let I be Ideal of L; ::_thesis: {(Bottom L)} c= I
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(Bottom L)} or a in I )
assume  a in {(Bottom L)} ; ::_thesis: a in I
then  a = Bottom L by TARSKI:def_1;
hence  a in I by Th21; ::_thesis: verum
end;


theorem Th25: :: WAYBEL_4:25
for L being lower-bounded sup-Semilattice holds the carrier of L --> {(Bottom L)} is Function of L,(InclPoset (Ids L))
proof
let L be lower-bounded sup-Semilattice; ::_thesis: the carrier of L --> {(Bottom L)} is Function of L,(InclPoset (Ids L))
 {(Bottom L)} = downarrow (Bottom L) by Th23;
then  {(Bottom L)} in  {  X where X is Ideal of L : verum  }  ;
then  {(Bottom L)} in the carrier of (InclPoset (Ids L)) by YELLOW_1:1;
hence  the carrier of L --> {(Bottom L)} is Function of L,(InclPoset (Ids L)) by FUNCOP_1:45; ::_thesis: verum
end;

Lm5:  for L being lower-bounded sup-Semilattice
for f being Function of L,(InclPoset (Ids L)) st f = the carrier of L --> {(Bottom L)} holds
f is monotone
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for f being Function of L,(InclPoset (Ids L)) st f = the carrier of L --> {(Bottom L)} holds
f is monotone
let f be Function of L,(InclPoset (Ids L)); ::_thesis: ( f = the carrier of L --> {(Bottom L)} implies f is monotone )
assume A1: f = the carrier of L --> {(Bottom L)} ; ::_thesis: f is monotone
let x, y be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
A2: f . x = {(Bottom L)} by A1, FUNCOP_1:7;
 f . y = {(Bottom L)} by A1, FUNCOP_1:7;
hence  ( not x <= y or for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) by A2, YELLOW_1:3; ::_thesis: verum
end;

theorem Th26: :: WAYBEL_4:26
for L being lower-bounded sup-Semilattice holds the carrier of L --> {(Bottom L)} in the carrier of (MonSet L)
proof
let L be lower-bounded sup-Semilattice; ::_thesis: the carrier of L --> {(Bottom L)} in the carrier of (MonSet L)
set s = the carrier of L --> {(Bottom L)};
 ex s9 being Function of L,(InclPoset (Ids L)) st
( the carrier of L --> {(Bottom L)} = s9 & s9 is monotone & ( for x being Element of L holds s9 . x c= downarrow x ) )
proof
reconsider s = the carrier of L --> {(Bottom L)} as Function of L,(InclPoset (Ids L)) by Th25;
take  s ; ::_thesis: ( the carrier of L --> {(Bottom L)} = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) )
 for x being Element of L holds s . x c= downarrow x
proof
let x be Element of L; ::_thesis: s . x c= downarrow x
 s . x = {(Bottom L)} by FUNCOP_1:7;
hence  s . x c= downarrow x by Lm4; ::_thesis: verum
end;
hence  ( the carrier of L --> {(Bottom L)} = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by Lm5; ::_thesis: verum
end;
hence  the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) by Def13; ::_thesis: verum
end;

theorem :: WAYBEL_4:27
for L being lower-bounded sup-Semilattice
for AR being auxiliary Relation of L holds [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L)
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for AR being auxiliary Relation of L holds [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L)
let AR be auxiliary Relation of L; ::_thesis: [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L)
set c = the carrier of L --> {(Bottom L)};
set d = AR -below ;
 ex f, g being Function of L,(InclPoset (Ids L)) st
( the carrier of L --> {(Bottom L)} = f & AR -below = g & the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) & AR -below in the carrier of (MonSet L) & f <= g )
proof
reconsider c = the carrier of L --> {(Bottom L)} as Function of L,(InclPoset (Ids L)) by Th25;
take  c ; ::_thesis: ex g being Function of L,(InclPoset (Ids L)) st
( the carrier of L --> {(Bottom L)} = c & AR -below = g & the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) & AR -below in the carrier of (MonSet L) & c <= g )
take  AR -below ; ::_thesis: ( the carrier of L --> {(Bottom L)} = c & AR -below = AR -below & the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) & AR -below in the carrier of (MonSet L) & c <= AR -below )
 c <= AR -below
proof
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 (InclPoset (Ids L)) st
( b1 = c . x & b2 = (AR -below) . x & b1 <= b2 ) )
assume  x in the carrier of L ; ::_thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = c . x & b2 = (AR -below) . x & b1 <= b2 )
then reconsider x9 = x as Element of L ;
 (AR -below) . x = AR -below x9 by Def12;
then reconsider dx = (AR -below) . x9 as Ideal of L ;
reconsider dx9 = dx as Element of (InclPoset (Ids L)) ;
 c . x9 = {(Bottom L)} by FUNCOP_1:7;
then A1: c . x c= dx by Lm4;
take  c . x9 ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Ids L)) st
( c . x9 = c . x & b1 = (AR -below) . x & c . x9 <= b1 )
take  dx9 ; ::_thesis: ( c . x9 = c . x & dx9 = (AR -below) . x & c . x9 <= dx9 )
thus  ( c . x9 = c . x & dx9 = (AR -below) . x & c . x9 <= dx9 ) by A1, YELLOW_1:3; ::_thesis: verum
end;
hence  ( the carrier of L --> {(Bottom L)} = c & AR -below = AR -below & the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) & AR -below in the carrier of (MonSet L) & c <= AR -below ) by Th18, Th26; ::_thesis: verum
end;
hence  [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L) by Def13; ::_thesis: verum
end;

Lm6:  for L being lower-bounded sup-Semilattice ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L)
proof
let L be lower-bounded sup-Semilattice; ::_thesis: ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L)
set x = IdsMap L;
reconsider x = IdsMap L as Element of (MonSet L) by Th19;
 x is_>=_than the carrier of (MonSet L)
proof
let b be Element of (MonSet L); :: according to LATTICE3:def_9 ::_thesis: ( not b in the carrier of (MonSet L) or b <= x )
assume  b in the carrier of (MonSet L) ; ::_thesis: b <= x
consider s being Function of L,(InclPoset (Ids L)) such that
A1: b = s and
 s is monotone and
A2: for x being Element of L holds s . x c= downarrow x by Def13;
 IdsMap L >= s
proof
let a be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not a in the carrier of L or ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . a & b2 = (IdsMap L) . a & b1 <= b2 ) )
assume  a in the carrier of L ; ::_thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . a & b2 = (IdsMap L) . a & b1 <= b2 )
then reconsider a9 = a as Element of L ;
A3: (IdsMap L) . a = downarrow a9 by YELLOW_2:def_4;
A4: s . a c= downarrow a9 by A2;
reconsider A = s . a9, B = (IdsMap L) . a9 as Element of (InclPoset (Ids L)) ;
take  A ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Ids L)) st
( A = s . a & b1 = (IdsMap L) . a & A <= b1 )
take  B ; ::_thesis: ( A = s . a & B = (IdsMap L) . a & A <= B )
thus  ( A = s . a & B = (IdsMap L) . a & A <= B ) by A3, A4, YELLOW_1:3; ::_thesis: verum
end;
then  [b,x] in the InternalRel of (MonSet L) by A1, Def13;
hence  b <= x by ORDERS_2:def_5; ::_thesis: verum
end;
hence  ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L) ; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
cluster MonSet L ->  strict upper-bounded ;
coherence
 MonSet L is upper-bounded
proof
consider x being Element of (MonSet L) such that
A1: x is_>=_than the carrier of (MonSet L) by Lm6;
take  x ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of (MonSet L) is_<=_than x
thus  the carrier of (MonSet L) is_<=_than x by A1; ::_thesis: verum
end;
end;

definition
let L be lower-bounded sup-Semilattice;
func Rel2Map L ->  Function of (InclPoset (Aux L)),(MonSet L) means :Def14: :: WAYBEL_4:def 14
 for AR being auxiliary Relation of L holds it . AR = AR -below ;
existence
 ex b1 being Function of (InclPoset (Aux L)),(MonSet L) st
for AR being auxiliary Relation of L holds b1 . AR = AR -below
proof
defpred S1[ set , set ] means  ex AR being auxiliary Relation of L st
( AR = $1 & $2 = AR -below );
A1: for a being set st a in the carrier of (InclPoset (Aux L)) holds
ex y being set st
( y in the carrier of (MonSet L) & S1[a,y] )
proof
let a be set ; ::_thesis: ( a in the carrier of (InclPoset (Aux L)) implies ex y being set st
( y in the carrier of (MonSet L) & S1[a,y] ) )
assume  a in the carrier of (InclPoset (Aux L)) ; ::_thesis: ex y being set st
( y in the carrier of (MonSet L) & S1[a,y] )
then  a in Aux L by YELLOW_1:1;
then reconsider AR = a as auxiliary Relation of L by Def8;
take  AR -below ; ::_thesis: ( AR -below in the carrier of (MonSet L) & S1[a,AR -below ] )
thus  ( AR -below in the carrier of (MonSet L) & S1[a,AR -below ] ) by Th18; ::_thesis: verum
end;
consider f being Function of the carrier of (InclPoset (Aux L)), the carrier of (MonSet L) such that
A2: for a being set st a in the carrier of (InclPoset (Aux L)) holds
S1[a,f . a] from FUNCT_2:sch_1(A1);
take  f ; ::_thesis: for AR being auxiliary Relation of L holds f . AR = AR -below
now__::_thesis:_for_AR_being_auxiliary_Relation_of_L_holds_f_._AR_=_AR_-below
let AR be auxiliary Relation of L; ::_thesis: f . AR = AR -below
 AR in Aux L by Def8;
then  AR in the carrier of (InclPoset (Aux L)) by YELLOW_1:1;
then  S1[AR,f . AR] by A2;
hence  f . AR = AR -below ; ::_thesis: verum
end;
hence  for AR being auxiliary Relation of L holds f . AR = AR -below ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (InclPoset (Aux L)),(MonSet L) st ( for AR being auxiliary Relation of L holds b1 . AR = AR -below ) & ( for AR being auxiliary Relation of L holds b2 . AR = AR -below ) holds
b1 = b2
proof
let I1, I2 be Function of (InclPoset (Aux L)),(MonSet L); ::_thesis: ( ( for AR being auxiliary Relation of L holds I1 . AR = AR -below ) & ( for AR being auxiliary Relation of L holds I2 . AR = AR -below ) implies I1 = I2 )
assume A3: for AR being auxiliary Relation of L holds I1 . AR = AR -below ; ::_thesis: ( ex AR being auxiliary Relation of L st not I2 . AR = AR -below or I1 = I2 )
assume A4: for AR being auxiliary Relation of L holds I2 . AR = AR -below ; ::_thesis: I1 = I2
 dom I1 = the carrier of (InclPoset (Aux L)) by FUNCT_2:def_1;
then A5: dom I1 = Aux L by YELLOW_1:1;
 dom I2 = the carrier of (InclPoset (Aux L)) by FUNCT_2:def_1;
then A6: dom I2 = Aux L by YELLOW_1:1;
now__::_thesis:_for_a_being_set_st_a_in_Aux_L_holds_
I1_._a_=_I2_._a
let a be set ; ::_thesis: ( a in Aux L implies I1 . a = I2 . a )
assume  a in Aux L ; ::_thesis: I1 . a = I2 . a
then reconsider AR = a as auxiliary Relation of L by Def8;
I1 . AR = AR -below by A3
.= I2 . AR by A4 ;
hence  I1 . a = I2 . a ; ::_thesis: verum
end;
hence  I1 = I2 by A5, A6, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines Rel2Map WAYBEL_4:def_14_:_
 for L being lower-bounded sup-Semilattice
for b2 being Function of (InclPoset (Aux L)),(MonSet L) holds
( b2 = Rel2Map L iff for AR being auxiliary Relation of L holds b2 . AR = AR -below );

theorem :: WAYBEL_4:28
for L being lower-bounded sup-Semilattice
for R1, R2 being auxiliary Relation of L st R1 c= R2 holds
R1 -below <= R2 -below
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for R1, R2 being auxiliary Relation of L st R1 c= R2 holds
R1 -below <= R2 -below
let R1, R2 be auxiliary Relation of L; ::_thesis: ( R1 c= R2 implies R1 -below <= R2 -below )
assume A1: R1 c= R2 ; ::_thesis: R1 -below <= R2 -below
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 (InclPoset (Ids L)) st
( b1 = (R1 -below) . x & b2 = (R2 -below) . x & b1 <= b2 ) )
assume  x in the carrier of L ; ::_thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = (R1 -below) . x & b2 = (R2 -below) . x & b1 <= b2 )
then reconsider x9 = x as Element of L ;
A2: R1 -below x9 c= R2 -below x9
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in R1 -below x9 or a in R2 -below x9 )
assume  a in R1 -below x9 ; ::_thesis: a in R2 -below x9
then  ex b being Element of L st
( b = a & [b,x9] in R1 ) ;
hence  a in R2 -below x9 by A1; ::_thesis: verum
end;
reconsider A1 = (R1 -below) . x9, A2 = (R2 -below) . x9 as Element of (InclPoset (Ids L)) ;
take  A1 ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Ids L)) st
( A1 = (R1 -below) . x & b1 = (R2 -below) . x & A1 <= b1 )
take  A2 ; ::_thesis: ( A1 = (R1 -below) . x & A2 = (R2 -below) . x & A1 <= A2 )
A3: (R1 -below) . x = R1 -below x9 by Def12;
 (R2 -below) . x = R2 -below x9 by Def12;
hence  ( A1 = (R1 -below) . x & A2 = (R2 -below) . x & A1 <= A2 ) by A2, A3, YELLOW_1:3; ::_thesis: verum
end;

theorem Th29: :: WAYBEL_4:29
for L being lower-bounded sup-Semilattice
for x being Element of L
for R1, R2 being Relation of L st R1 c= R2 holds
R1 -below x c= R2 -below x
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for x being Element of L
for R1, R2 being Relation of L st R1 c= R2 holds
R1 -below x c= R2 -below x
let x be Element of L; ::_thesis: for R1, R2 being Relation of L st R1 c= R2 holds
R1 -below x c= R2 -below x
let R1, R2 be Relation of L; ::_thesis: ( R1 c= R2 implies R1 -below x c= R2 -below x )
assume A1: R1 c= R2 ; ::_thesis: R1 -below x c= R2 -below x
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in R1 -below x or a in R2 -below x )
assume  a in R1 -below x ; ::_thesis: a in R2 -below x
then  ex b being Element of L st
( b = a & [b,x] in R1 ) ;
hence  a in R2 -below x by A1; ::_thesis: verum
end;

Lm7:  for L being lower-bounded sup-Semilattice holds Rel2Map L is monotone
proof
let L be lower-bounded sup-Semilattice; ::_thesis: Rel2Map L is monotone
let x, y be Element of (InclPoset (Aux L)); :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (MonSet L) holds
( not b1 = (Rel2Map L) . x or not b2 = (Rel2Map L) . y or b1 <= b2 ) )
A1: x in the carrier of (InclPoset (Aux L)) ;
A2: y in the carrier of (InclPoset (Aux L)) ;
A3: x in Aux L by A1, YELLOW_1:1;
 y in Aux L by A2, YELLOW_1:1;
then reconsider R1 = x, R2 = y as auxiliary Relation of L by A3, Def8;
assume  x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (MonSet L) holds
( not b1 = (Rel2Map L) . x or not b2 = (Rel2Map L) . y or b1 <= b2 )
then A4: x c= y by YELLOW_1:3;
let a, b be Element of (MonSet L); ::_thesis: ( not a = (Rel2Map L) . x or not b = (Rel2Map L) . y or a <= b )
assume that
A5: a = (Rel2Map L) . x and
A6: b = (Rel2Map L) . y ; ::_thesis: a <= b
thus  a <= b ::_thesis: verum
proof
A7: (Rel2Map L) . x = R1 -below by Def14;
A8: (Rel2Map L) . y = R2 -below by Def14;
consider s being Function of L,(InclPoset (Ids L)) such that
A9: (Rel2Map L) . x = s and
 s is monotone and
 for x being Element of L holds s . x c= downarrow x by Def13;
consider t being Function of L,(InclPoset (Ids L)) such that
A10: (Rel2Map L) . y = t and
 t is monotone and
 for x being Element of L holds t . x c= downarrow x by Def13;
 s <= t
proof
let q be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not q in the carrier of L or ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . q & b2 = t . q & b1 <= b2 ) )
assume  q in the carrier of L ; ::_thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . q & b2 = t . q & b1 <= b2 )
then reconsider q9 = q as Element of L ;
A11: s . q = R1 -below q9 by A7, A9, Def12;
A12: t . q = R2 -below q9 by A8, A10, Def12;
A13: R1 -below q9 c= R2 -below q9 by A4, Th29;
reconsider sq = s . q9, tq = t . q9 as Element of (InclPoset (Ids L)) ;
 sq <= tq by A11, A12, A13, YELLOW_1:3;
hence  ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . q & b2 = t . q & b1 <= b2 ) ; ::_thesis: verum
end;
then  [(R1 -below),(R2 -below)] in the InternalRel of (MonSet L) by A7, A8, A9, A10, Def13;
hence  a <= b by A5, A6, A7, A8, ORDERS_2:def_5; ::_thesis: verum
end;
end;

registration
let L be lower-bounded sup-Semilattice;
cluster Rel2Map L ->  monotone ;
coherence
 Rel2Map L is monotone by Lm7;
end;

definition
let L be lower-bounded sup-Semilattice;
func Map2Rel L ->  Function of (MonSet L),(InclPoset (Aux L)) means :Def15: :: WAYBEL_4:def 15
 for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = it . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) );
existence
 ex b1 being Function of (MonSet L),(InclPoset (Aux L)) st
for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b1 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
proof
defpred S1[ set , set ] means  ex AR being auxiliary Relation of L st
( AR = $2 & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = $1 & x9 in s9 . y9 ) ) ) );
A1: for a being set st a in the carrier of (MonSet L) holds
ex b being set st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
proof
let a be set ; ::_thesis: ( a in the carrier of (MonSet L) implies ex b being set st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] ) )
assume A2: a in the carrier of (MonSet L) ; ::_thesis: ex b being set st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
defpred S2[ set , set ] means  ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = $1 & y9 = $2 & s9 = a & x9 in s9 . y9 );
consider R being Relation of the carrier of L, the carrier of L such that
A3: for x, y being set holds
( [x,y] in R iff ( x in the carrier of L & y in the carrier of L & S2[x,y] ) ) from RELSET_1:sch_1();
reconsider R = R as Relation of L ;
A4: R is auxiliary(i)
proof
let x, y be Element of L; :: according to WAYBEL_4:def_3 ::_thesis: ( [x,y] in R implies x <= y )
assume  [x,y] in R ; ::_thesis: x <= y
then consider x9, y9 being Element of L, s9 being Function of L,(InclPoset (Ids L)) such that
A5: x9 = x and
A6: y9 = y and
A7: s9 = a and
A8: x9 in s9 . y9 by A3;
 ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by A2, Def13;
then  s9 . y c= downarrow y by A7;
hence  x <= y by A5, A6, A8, WAYBEL_0:17; ::_thesis: verum
end;
A9: R is auxiliary(ii)
proof
let x, y, z, u be Element of L; :: according to WAYBEL_4:def_4 ::_thesis: ( u <= x & [x,y] in R & y <= z implies [u,z] in R )
assume that
A10: u <= x and
A11: [x,y] in R and
A12: y <= z ; ::_thesis: [u,z] in R
A13: ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = a & x9 in s9 . y9 ) by A3, A11;
consider s being Function of L,(InclPoset (Ids L)) such that
A14: a = s and
A15: s is monotone and
 for x being Element of L holds s . x c= downarrow x by A2, Def13;
reconsider sy = s . y, sz = s . z as Element of (InclPoset (Ids L)) ;
 sy <= sz by A12, A15, ORDERS_3:def_5;
then A16: s . y c= s . z by YELLOW_1:3;
 s . z in the carrier of (InclPoset (Ids L)) ;
then  s . z in Ids L by YELLOW_1:1;
then consider sz being Ideal of L such that
A17: s . z = sz ;
 u in sz by A10, A13, A14, A16, A17, WAYBEL_0:def_19;
hence  [u,z] in R by A3, A14, A17; ::_thesis: verum
end;
A18: R is auxiliary(iii)
proof
let x, y, z be Element of L; :: according to WAYBEL_4:def_5 ::_thesis: ( [x,z] in R & [y,z] in R implies [(x "\/" y),z] in R )
assume that
A19: [x,z] in R and
A20: [y,z] in R ; ::_thesis: [(x "\/" y),z] in R
consider x1, z1 being Element of L, s1 being Function of L,(InclPoset (Ids L)) such that
A21: x1 = x and
A22: z1 = z and
A23: s1 = a and
A24: x1 in s1 . z1 by A3, A19;
A25: ex y2, z2 being Element of L ex s2 being Function of L,(InclPoset (Ids L)) st
( y2 = y & z2 = z & s2 = a & y2 in s2 . z2 ) by A3, A20;
 s1 . z in the carrier of (InclPoset (Ids L)) ;
then  s1 . z in Ids L by YELLOW_1:1;
then consider sz being Ideal of L such that
A26: s1 . z = sz ;
consider z3 being Element of L such that
A27: z3 in sz and
A28: x <= z3 and
A29: y <= z3 by A21, A22, A23, A24, A25, A26, WAYBEL_0:def_1;
 ex q being Element of L st
( x <= q & y <= q & ( for c being Element of L st x <= c & y <= c holds
q <= c ) ) by LATTICE3:def_10;
then  x "\/" y <= z3 by A28, A29, LATTICE3:def_13;
then  x "\/" y in sz by A27, WAYBEL_0:def_19;
hence  [(x "\/" y),z] in R by A3, A23, A26; ::_thesis: verum
end;
 R is auxiliary(iv)
proof
let x be Element of L; :: according to WAYBEL_4:def_6 ::_thesis: [(Bottom L),x] in R
reconsider x9 = Bottom L, y9 = x as Element of L ;
consider s9 being Function of L,(InclPoset (Ids L)) such that
A30: a = s9 and
 s9 is monotone and
 for x being Element of L holds s9 . x c= downarrow x by A2, Def13;
 s9 . y9 in the carrier of (InclPoset (Ids L)) ;
then  s9 . y9 in Ids L by YELLOW_1:1;
then consider sy being Ideal of L such that
A31: sy = s9 . y9 ;
 x9 in sy by Th21;
hence  [(Bottom L),x] in R by A3, A30, A31; ::_thesis: verum
end;
then reconsider R = R as auxiliary Relation of L by A4, A9, A18;
A32: for x, y being set holds
( [x,y] in R iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = a & x9 in s9 . y9 ) ) by A3;
take b = R; ::_thesis: ( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
 b in Aux L by Def8;
hence  ( b in the carrier of (InclPoset (Aux L)) & S1[a,b] ) by A32, YELLOW_1:1; ::_thesis: verum
end;
consider f being Function of the carrier of (MonSet L), the carrier of (InclPoset (Aux L)) such that
A33: for a being set st a in the carrier of (MonSet L) holds
S1[a,f . a] from FUNCT_2:sch_1(A1);
reconsider f9 = f as Function of (MonSet L),(InclPoset (Aux L)) ;
take  f9 ; ::_thesis: for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = f9 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
let s be set ; ::_thesis: ( s in the carrier of (MonSet L) implies ex AR being auxiliary Relation of L st
( AR = f9 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) )
assume A34: s in the carrier of (MonSet L) ; ::_thesis: ex AR being auxiliary Relation of L st
( AR = f9 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
then reconsider s9 = s as Element of (MonSet L) ;
 f9 . s9 in the carrier of (InclPoset (Aux L)) ;
then  f9 . s9 in Aux L by YELLOW_1:1;
then reconsider fs = f9 . s9 as auxiliary Relation of L by Def8;
take  fs ; ::_thesis: ( fs = f9 . s & ( for x, y being set holds
( [x,y] in fs iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
 ex AR being auxiliary Relation of L st
( AR = f9 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) by A33, A34;
hence  ( fs = f9 . s & ( for x, y being set holds
( [x,y] in fs iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (MonSet L),(InclPoset (Aux L)) st ( for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b1 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) & ( for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b2 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) holds
b1 = b2
proof
let M1, M2 be Function of (MonSet L),(InclPoset (Aux L)); ::_thesis: ( ( for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = M1 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) & ( for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = M2 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) implies M1 = M2 )
assume A35: for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = M1 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ; ::_thesis: ( ex s being set st
( s in the carrier of (MonSet L) & ( for AR being auxiliary Relation of L holds
( not AR = M2 . s or ex x, y being set st
( ( [x,y] in AR implies ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) implies ( ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) & not [x,y] in AR ) ) ) ) ) or M1 = M2 )
assume A36: for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = M2 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ; ::_thesis: M1 = M2
A37: dom M1 = the carrier of (MonSet L) by FUNCT_2:def_1;
A38: dom M2 = the carrier of (MonSet L) by FUNCT_2:def_1;
 for s being set st s in the carrier of (MonSet L) holds
M1 . s = M2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of (MonSet L) implies M1 . s = M2 . s )
assume A39: s in the carrier of (MonSet L) ; ::_thesis: M1 . s = M2 . s
then consider AR1 being auxiliary Relation of L such that
A40: AR1 = M1 . s and
A41: for x, y being set holds
( [x,y] in AR1 iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) by A35;
consider AR2 being auxiliary Relation of L such that
A42: AR2 = M2 . s and
A43: for x, y being set holds
( [x,y] in AR2 iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) by A36, A39;
 AR1 = AR2
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in AR1 or [x,y] in AR2 ) & ( not [x,y] in AR2 or [x,y] in AR1 ) )
hereby  ::_thesis: ( not [x,y] in AR2 or [x,y] in AR1 )
assume  [x,y] in AR1 ; ::_thesis: [x,y] in AR2
then  ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) by A41;
hence  [x,y] in AR2 by A43; ::_thesis: verum
end;
assume  [x,y] in AR2 ; ::_thesis: [x,y] in AR1
then  ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) by A43;
hence  [x,y] in AR1 by A41; ::_thesis: verum
end;
hence  M1 . s = M2 . s by A40, A42; ::_thesis: verum
end;
hence  M1 = M2 by A37, A38, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines Map2Rel WAYBEL_4:def_15_:_
 for L being lower-bounded sup-Semilattice
for b2 being Function of (MonSet L),(InclPoset (Aux L)) holds
( b2 = Map2Rel L iff for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b2 . s & ( for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) );

Lm8:  for L being lower-bounded sup-Semilattice holds Map2Rel L is monotone
proof
let L be lower-bounded sup-Semilattice; ::_thesis: Map2Rel L is monotone
set f = Map2Rel L;
A1: InclPoset (Aux L) = RelStr(# (Aux L),(RelIncl (Aux L)) #) by YELLOW_1:def_1;
let x, y be Element of (MonSet L); :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 ) )
assume  x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 )
then  [x,y] in the InternalRel of (MonSet L) by ORDERS_2:def_5;
then consider s, t being Function of L,(InclPoset (Ids L)) such that
A2: x = s and
A3: y = t and
 x in the carrier of (MonSet L) and
 y in the carrier of (MonSet L) and
A4: s <= t by Def13;
A5: (Map2Rel L) . s in the carrier of (InclPoset (Aux L)) by A2, FUNCT_2:5;
A6: (Map2Rel L) . t in the carrier of (InclPoset (Aux L)) by A3, FUNCT_2:5;
A7: (Map2Rel L) . s in Aux L by A5, YELLOW_1:1;
A8: (Map2Rel L) . t in Aux L by A6, YELLOW_1:1;
then reconsider AS = (Map2Rel L) . s, AT = (Map2Rel L) . t as auxiliary Relation of L by A7, Def8;
reconsider AS9 = AS, AT9 = AT as Element of (InclPoset (Aux L)) by A2, A3, FUNCT_2:5;
 for a, b being set st [a,b] in AS holds
[a,b] in AT
proof
let a, b be set ; ::_thesis: ( [a,b] in AS implies [a,b] in AT )
assume A9: [a,b] in AS ; ::_thesis: [a,b] in AT
then A10: b in the carrier of L by ZFMISC_1:87;
reconsider a9 = a, b9 = b as Element of L by A9, ZFMISC_1:87;
reconsider sb = s . b9, tb = t . b9 as Element of (InclPoset (Ids L)) ;
 ex a1, b1 being Element of (InclPoset (Ids L)) st
( a1 = s . b & b1 = t . b & a1 <= b1 ) by A4, A10, YELLOW_2:def_1;
then A11: sb c= tb by YELLOW_1:3;
 ex AR being auxiliary Relation of L st
( AR = (Map2Rel L) . x & ( for a9, b9 being set holds
( [a9,b9] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a9 & y9 = b9 & s9 = x & x9 in s9 . y9 ) ) ) ) by Def15;
then A12: ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a9 & y9 = b9 & s9 = s & x9 in s9 . y9 ) by A2, A9;
 ex AR1 being auxiliary Relation of L st
( AR1 = (Map2Rel L) . y & ( for a9, b9 being set holds
( [a9,b9] in AR1 iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a9 & y9 = b9 & s9 = y & x9 in s9 . y9 ) ) ) ) by Def15;
hence  [a,b] in AT by A3, A11, A12; ::_thesis: verum
end;
then  AS9 c= AT9 by RELAT_1:def_3;
then  [AS9,AT9] in RelIncl (Aux L) by A7, A8, WELLORD2:def_1;
hence  for b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 ) by A1, A2, A3, ORDERS_2:def_5; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
cluster Map2Rel L ->  monotone ;
coherence
 Map2Rel L is monotone by Lm8;
end;

theorem Th30: :: WAYBEL_4:30
for L being lower-bounded sup-Semilattice holds (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))
proof
let L be lower-bounded sup-Semilattice; ::_thesis: (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))
set LS = (Map2Rel L) * (Rel2Map L);
set R = id (dom (Rel2Map L));
 dom ((Map2Rel L) * (Rel2Map L)) = the carrier of (InclPoset (Aux L)) by FUNCT_2:def_1;
then A1: dom ((Map2Rel L) * (Rel2Map L)) = Aux L by YELLOW_1:1;
 dom (id (dom (Rel2Map L))) = the carrier of (InclPoset (Aux L)) by FUNCT_2:def_1;
then A2: dom (id (dom (Rel2Map L))) = Aux L by YELLOW_1:1;
 for a being set st a in Aux L holds
((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a
proof
let a be set ; ::_thesis: ( a in Aux L implies ((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a )
assume A3: a in Aux L ; ::_thesis: ((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a
then reconsider AR = a as auxiliary Relation of L by Def8;
A4: a in the carrier of (InclPoset (Aux L)) by A3, YELLOW_1:1;
then A5: a in dom (Rel2Map L) by FUNCT_2:def_1;
then  ((Map2Rel L) * (Rel2Map L)) . a = (Map2Rel L) . ((Rel2Map L) . AR) by FUNCT_1:13;
then A6: ((Map2Rel L) * (Rel2Map L)) . a = (Map2Rel L) . (AR -below) by Def14;
 ((Map2Rel L) * (Rel2Map L)) . a in the carrier of (InclPoset (Aux L)) by A4, FUNCT_2:5;
then  ((Map2Rel L) * (Rel2Map L)) . a in Aux L by YELLOW_1:1;
then reconsider La = ((Map2Rel L) * (Rel2Map L)) . a as auxiliary Relation of L by Def8;
A7: AR -below in the carrier of (MonSet L) by Th18;
 for c, b being set holds
( [c,b] in La iff [c,b] in AR )
proof
let c, b be set ; ::_thesis: ( [c,b] in La iff [c,b] in AR )
hereby  ::_thesis: ( [c,b] in AR implies [c,b] in La )
assume A8: [c,b] in La ; ::_thesis: [c,b] in AR
 ex AR9 being auxiliary Relation of L st
( AR9 = (Map2Rel L) . (AR -below) & ( for c, b being set holds
( [c,b] in AR9 iff ex c9, b9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( c9 = c & b9 = b & s9 = AR -below & c9 in s9 . b9 ) ) ) ) by A7, Def15;
then consider c9, b9 being Element of L, s9 being Function of L,(InclPoset (Ids L)) such that
A9: c9 = c and
A10: b9 = b and
A11: s9 = AR -below and
A12: c9 in s9 . b9 by A6, A8;
 c9 in AR -below b9 by A11, A12, Def12;
hence  [c,b] in AR by A9, A10, Th13; ::_thesis: verum
end;
assume A13: [c,b] in AR ; ::_thesis: [c,b] in La
then reconsider c9 = c, b9 = b as Element of L by ZFMISC_1:87;
 c9 in AR -below b9 by A13;
then A14: c9 in (AR -below) . b9 by Def12;
 ex AR9 being auxiliary Relation of L st
( AR9 = (Map2Rel L) . (AR -below) & ( for c, b being set holds
( [c,b] in AR9 iff ex c9, b9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( c9 = c & b9 = b & s9 = AR -below & c9 in s9 . b9 ) ) ) ) by A7, Def15;
hence  [c,b] in La by A6, A14; ::_thesis: verum
end;
then  La = AR by RELAT_1:def_2;
hence  ((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a by A5, FUNCT_1:18; ::_thesis: verum
end;
hence  (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L)) by A1, A2, FUNCT_1:2; ::_thesis: verum
end;

theorem Th31: :: WAYBEL_4:31
for L being lower-bounded sup-Semilattice holds (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)
proof
let L be lower-bounded sup-Semilattice; ::_thesis: (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)
set LS = (Rel2Map L) * (Map2Rel L);
set R = id the carrier of (MonSet L);
A1: dom ((Rel2Map L) * (Map2Rel L)) = the carrier of (MonSet L) by FUNCT_2:def_1;
A2: dom (id the carrier of (MonSet L)) = the carrier of (MonSet L) ;
 for a being set st a in the carrier of (MonSet L) holds
((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a
proof
let a be set ; ::_thesis: ( a in the carrier of (MonSet L) implies ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a )
assume A3: a in the carrier of (MonSet L) ; ::_thesis: ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a
then consider s being Function of L,(InclPoset (Ids L)) such that
A4: a = s and
 s is monotone and
 for x being Element of L holds s . x c= downarrow x by Def13;
 ((Rel2Map L) * (Map2Rel L)) . s in the carrier of (MonSet L) by A3, A4, FUNCT_2:5;
then consider Ls being Function of L,(InclPoset (Ids L)) such that
A5: ((Rel2Map L) * (Map2Rel L)) . s = Ls and
 Ls is monotone and
 for x being Element of L holds Ls . x c= downarrow x by Def13;
set AR = (Map2Rel L) . s;
 (Map2Rel L) . s in the carrier of (InclPoset (Aux L)) by A3, A4, FUNCT_2:5;
then  (Map2Rel L) . s in Aux L by YELLOW_1:1;
then reconsider AR = (Map2Rel L) . s as auxiliary Relation of L by Def8;
 dom (Map2Rel L) = the carrier of (MonSet L) by FUNCT_2:def_1;
then  Ls = (Rel2Map L) . AR by A3, A4, A5, FUNCT_1:13;
then A6: Ls = AR -below by Def14;
A7: dom Ls = the carrier of L by FUNCT_2:def_1;
A8: dom s = the carrier of L by FUNCT_2:def_1;
now__::_thesis:_for_b_being_set_st_b_in_the_carrier_of_L_holds_
Ls_._b_=_s_._b
let b be set ; ::_thesis: ( b in the carrier of L implies Ls . b = s . b )
assume A9: b in the carrier of L ; ::_thesis: Ls . b = s . b
then reconsider b9 = b as Element of L ;
A10: Ls . b c= s . b
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in Ls . b or d in s . b )
assume  d in Ls . b ; ::_thesis: d in s . b
then  d in AR -below b9 by A6, Def12;
then A11: [d,b9] in AR by Th13;
 ex AR9 being auxiliary Relation of L st
( AR9 = (Map2Rel L) . s & ( for d, b9 being set holds
( [d,b9] in AR9 iff ex d9, b99 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( d9 = d & b99 = b9 & s9 = s & d9 in s9 . b99 ) ) ) ) by A3, A4, Def15;
then  ex d9, b99 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( d9 = d & b99 = b9 & s9 = s & d9 in s9 . b99 ) by A11;
hence  d in s . b ; ::_thesis: verum
end;
 s . b c= Ls . b
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in s . b or d in Ls . b )
assume A12: d in s . b ; ::_thesis: d in Ls . b
 s . b in the carrier of (InclPoset (Ids L)) by A9, FUNCT_2:5;
then  s . b in Ids L by YELLOW_1:1;
then  ex X being Ideal of L st s . b = X ;
then reconsider d9 = d as Element of L by A12;
 ex AR9 being auxiliary Relation of L st
( AR9 = (Map2Rel L) . s & ( for d, b9 being set holds
( [d,b9] in AR9 iff ex d9, b99 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( d9 = d & b99 = b9 & s9 = s & d9 in s9 . b99 ) ) ) ) by A3, A4, Def15;
then  [d9,b9] in AR by A12;
then  d9 in AR -below b9 ;
hence  d in Ls . b by A6, Def12; ::_thesis: verum
end;
hence  Ls . b = s . b by A10, XBOOLE_0:def_10; ::_thesis: verum
end;
then  Ls = s by A7, A8, FUNCT_1:2;
hence  ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a by A3, A4, A5, FUNCT_1:18; ::_thesis: verum
end;
hence  (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L) by A1, A2, FUNCT_1:2; ::_thesis: verum
end;

registration
let L be lower-bounded sup-Semilattice;
cluster Rel2Map L -> V16() ;
coherence
 Rel2Map L is one-to-one
proof
 ex g being Function st g * (Rel2Map L) = id (dom (Rel2Map L))
proof
take  Map2Rel L ; ::_thesis: (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))
thus  (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L)) by Th30; ::_thesis: verum
end;
hence  Rel2Map L is one-to-one by FUNCT_1:31; ::_thesis: verum
end;
end;

theorem Th32: :: WAYBEL_4:32
for L being lower-bounded sup-Semilattice holds (Rel2Map L) " = Map2Rel L
proof
let L be lower-bounded sup-Semilattice; ::_thesis: (Rel2Map L) " = Map2Rel L
 ( (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L) implies rng (Rel2Map L) = the carrier of (MonSet L) ) by FUNCT_2:18;
then A1: rng (Rel2Map L) = dom (Map2Rel L) by Th31, FUNCT_2:def_1;
 (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L)) by Th30;
hence  (Rel2Map L) " = Map2Rel L by A1, FUNCT_1:41; ::_thesis: verum
end;

theorem :: WAYBEL_4:33
for L being lower-bounded sup-Semilattice holds Rel2Map L is isomorphic
proof
let L be lower-bounded sup-Semilattice; ::_thesis: Rel2Map L is isomorphic
 ex g being Function of (MonSet L),(InclPoset (Aux L)) st
( g = (Rel2Map L) " & g is monotone )
proof
reconsider g = Map2Rel L as Function of (MonSet L),(InclPoset (Aux L)) ;
take  g ; ::_thesis: ( g = (Rel2Map L) " & g is monotone )
thus  ( g = (Rel2Map L) " & g is monotone ) by Th32; ::_thesis: verum
end;
hence  Rel2Map L is isomorphic by WAYBEL_0:def_38; ::_thesis: verum
end;

theorem Th34: :: WAYBEL_4:34
for L being complete LATTICE
for x being Element of L holds meet  {  I where I is Ideal of L : x <= sup I  }  = waybelow x
proof
let L be complete LATTICE; ::_thesis: for x being Element of L holds meet  {  I where I is Ideal of L : x <= sup I  }  = waybelow x
let x be Element of L; ::_thesis: meet  {  I where I is Ideal of L : x <= sup I  }  = waybelow x
set X =  {  I where I is Ideal of L : x <= sup I  }  ;
  {  I where I is Ideal of L : x <= sup I  }  c= bool the carrier of L
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  I where I is Ideal of L : x <= sup I  }  or a in bool the carrier of L )
assume  a in  {  I where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in bool the carrier of L
then  ex I being Ideal of L st
( a = I & x <= sup I ) ;
hence  a in bool the carrier of L ; ::_thesis: verum
end;
then reconsider X9 =  {  I where I is Ideal of L : x <= sup I  }  as Subset-Family of L ;
 sup (downarrow x) = x by WAYBEL_0:34;
then A1: downarrow x in  {  I where I is Ideal of L : x <= sup I  }  ;
thus  meet  {  I where I is Ideal of L : x <= sup I  }  c= waybelow x :: according to XBOOLE_0:def_10 ::_thesis: waybelow x c= meet  {  I where I is Ideal of L : x <= sup I  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in meet  {  I where I is Ideal of L : x <= sup I  }  or a in waybelow x )
assume A2: a in meet  {  I where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in waybelow x
then  a in meet X9 ;
then reconsider y = a as Element of L ;
now__::_thesis:_for_I_being_Ideal_of_L_st_x_<=_sup_I_holds_
y_in_I
let I be Ideal of L; ::_thesis: ( x <= sup I implies y in I )
assume  x <= sup I ; ::_thesis: y in I
then  I in  {  I where I is Ideal of L : x <= sup I  }  ;
hence  y in I by A2, SETFAM_1:def_1; ::_thesis: verum
end;
then  y << x by WAYBEL_3:21;
hence  a in waybelow x by WAYBEL_3:7; ::_thesis: verum
end;
thus  waybelow x c= meet  {  I where I is Ideal of L : x <= sup I  }  ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in waybelow x or a in meet  {  I where I is Ideal of L : x <= sup I  }  )
assume  a in waybelow x ; ::_thesis: a in meet  {  I where I is Ideal of L : x <= sup I  }
then  a in  {  y where y is Element of L : y << x  }  by WAYBEL_3:def_3;
then A3: ex a9 being Element of L st
( a9 = a & a9 << x ) ;
 for Y being set st Y in  {  I where I is Ideal of L : x <= sup I  }  holds
a in Y
proof
let Y be set ; ::_thesis: ( Y in  {  I where I is Ideal of L : x <= sup I  }  implies a in Y )
assume  Y in  {  I where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in Y
then  ex I being Ideal of L st
( Y = I & x <= sup I ) ;
hence  a in Y by A3, WAYBEL_3:20; ::_thesis: verum
end;
hence  a in meet  {  I where I is Ideal of L : x <= sup I  }  by A1, SETFAM_1:def_1; ::_thesis: verum
end;
end;

definition
let L be Semilattice;
let I be Ideal of L;
func DownMap I ->  Function of L,(InclPoset (Ids L)) means :Def16: :: WAYBEL_4:def 16
 for x being Element of L holds
( ( x <= sup I implies it . x = (downarrow x) /\ I ) & ( not x <= sup I implies it . x = downarrow x ) );
existence
 ex b1 being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds
( ( x <= sup I implies b1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b1 . x = downarrow x ) )
proof
defpred S1[ set , set ] means  for x being Element of L st x = $1 holds
( ( x <= sup I implies $2 = (downarrow x) /\ I ) & ( not x <= sup I implies $2 = downarrow x ) );
defpred S2[ Element of L] means $1 <= sup I;
deffunc H1( Element of L) ->  Element of bool the carrier of L = (downarrow $1) /\ I;
deffunc H2( Element of L) ->  Element of bool the carrier of L = downarrow $1;
consider f being Function such that
A1: ( dom f = the carrier of L & ( for x being Element of L holds
( ( S2[x] implies f . x = H1(x) ) & ( not S2[x] implies f . x = H2(x) ) ) ) ) from PARTFUN1:sch_4();
A2: for a being set st a in the carrier of L holds
ex y being set st
( y in the carrier of (InclPoset (Ids L)) & S1[a,y] )
proof
let a be set ; ::_thesis: ( a in the carrier of L implies ex y being set st
( y in the carrier of (InclPoset (Ids L)) & S1[a,y] ) )
assume  a in the carrier of L ; ::_thesis: ex y being set st
( y in the carrier of (InclPoset (Ids L)) & S1[a,y] )
then reconsider x = a as Element of L ;
take y = f . x; ::_thesis: ( y in the carrier of (InclPoset (Ids L)) & S1[a,y] )
thus  y in the carrier of (InclPoset (Ids L)) ::_thesis: S1[a,y]
proof
percases ( x <= sup I or not x <= sup I ) ;
suppose x <= sup I ; ::_thesis: y in the carrier of (InclPoset (Ids L))
then  y = (downarrow x) /\ I by A1;
then  y is Ideal of L by YELLOW_2:40;
then  y in  {  X where X is Ideal of L : verum  }  ;
hence  y in the carrier of (InclPoset (Ids L)) by YELLOW_1:1; ::_thesis: verum
end;
suppose not x <= sup I ; ::_thesis: y in the carrier of (InclPoset (Ids L))
then  y = downarrow x by A1;
then  y in  {  X where X is Ideal of L : verum  }  ;
hence  y in the carrier of (InclPoset (Ids L)) by YELLOW_1:1; ::_thesis: verum
end;
end;
end;
thus  S1[a,y] by A1; ::_thesis: verum
end;
consider f being Function of the carrier of L, the carrier of (InclPoset (Ids L)) such that
A3: for a being set st a in the carrier of L holds
S1[a,f . a] from FUNCT_2:sch_1(A2);
reconsider f = f as Function of L,(InclPoset (Ids L)) ;
 for x being Element of L holds
( ( x <= sup I implies f . x = (downarrow x) /\ I ) & ( not x <= sup I implies f . x = downarrow x ) ) by A3;
hence  ex b1 being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds
( ( x <= sup I implies b1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b1 . x = downarrow x ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds
( ( x <= sup I implies b1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b1 . x = downarrow x ) ) ) & ( for x being Element of L holds
( ( x <= sup I implies b2 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b2 . x = downarrow x ) ) ) holds
b1 = b2
proof
let M1, M2 be Function of L,(InclPoset (Ids L)); ::_thesis: ( ( for x being Element of L holds
( ( x <= sup I implies M1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies M1 . x = downarrow x ) ) ) & ( for x being Element of L holds
( ( x <= sup I implies M2 . x = (downarrow x) /\ I ) & ( not x <= sup I implies M2 . x = downarrow x ) ) ) implies M1 = M2 )
assume A4: for x being Element of L holds
( ( x <= sup I implies M1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies M1 . x = downarrow x ) ) ; ::_thesis: ( ex x being Element of L st
( ( x <= sup I implies M2 . x = (downarrow x) /\ I ) implies ( not x <= sup I & not M2 . x = downarrow x ) ) or M1 = M2 )
assume A5: for x being Element of L holds
( ( x <= sup I implies M2 . x = (downarrow x) /\ I ) & ( not x <= sup I implies M2 . x = downarrow x ) ) ; ::_thesis: M1 = M2
A6: dom M1 = the carrier of L by FUNCT_2:def_1;
A7: dom M2 = the carrier of L by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
M1_._x_=_M2_._x
let x be set ; ::_thesis: ( x in the carrier of L implies M1 . x = M2 . x )
assume  x in the carrier of L ; ::_thesis: M1 . x = M2 . x
then reconsider x9 = x as Element of L ;
A8: now__::_thesis:_(_x9_<=_sup_I_implies_M1_._x9_=_M2_._x9_)
assume A9: x9 <= sup I ; ::_thesis: M1 . x9 = M2 . x9
then  M1 . x9 = (downarrow x9) /\ I by A4;
hence  M1 . x9 = M2 . x9 by A5, A9; ::_thesis: verum
end;
now__::_thesis:_(_not_x9_<=_sup_I_implies_M1_._x9_=_M2_._x9_)
assume A10: not x9 <= sup I ; ::_thesis: M1 . x9 = M2 . x9
then  M1 . x9 = downarrow x9 by A4;
hence  M1 . x9 = M2 . x9 by A5, A10; ::_thesis: verum
end;
hence  M1 . x = M2 . x by A8; ::_thesis: verum
end;
hence  M1 = M2 by A6, A7, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines DownMap WAYBEL_4:def_16_:_
 for L being Semilattice
for I being Ideal of L
for b3 being Function of L,(InclPoset (Ids L)) holds
( b3 = DownMap I iff for x being Element of L holds
( ( x <= sup I implies b3 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b3 . x = downarrow x ) ) );

Lm9:  for L being Semilattice
for I being Ideal of L holds DownMap I is monotone
proof
let L be Semilattice; ::_thesis: for I being Ideal of L holds DownMap I is monotone
let I be Ideal of L; ::_thesis: DownMap I is monotone
let x, y be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 ) )
assume A1: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 )
percases ( ( x <= sup I & y <= sup I ) or ( x <= sup I & not y <= sup I ) or ( not x <= sup I & y <= sup I ) or ( not x <= sup I & not y <= sup I ) ) ;
supposeA2: ( x <= sup I & y <= sup I ) ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 )
then A3: (DownMap I) . x = (downarrow x) /\ I by Def16;
 (DownMap I) . y = (downarrow y) /\ I by A2, Def16;
then  (DownMap I) . x c= (DownMap I) . y by A1, A3, WAYBEL_0:21, XBOOLE_1:26;
hence  for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 ) by YELLOW_1:3; ::_thesis: verum
end;
supposeA4: ( x <= sup I & not y <= sup I ) ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 )
then A5: (DownMap I) . x = (downarrow x) /\ I by Def16;
A6: (DownMap I) . y = downarrow y by A4, Def16;
A7: downarrow x c= downarrow y by A1, WAYBEL_0:21;
 (downarrow x) /\ I c= downarrow x by XBOOLE_1:17;
then  (DownMap I) . x c= (DownMap I) . y by A5, A6, A7, XBOOLE_1:1;
hence  for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 ) by YELLOW_1:3; ::_thesis: verum
end;
suppose ( not x <= sup I & y <= sup I ) ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 )
hence  for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 ) by A1, ORDERS_2:3; ::_thesis: verum
end;
supposeA8: ( not x <= sup I & not y <= sup I ) ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 )
then A9: (DownMap I) . x = downarrow x by Def16;
 (DownMap I) . y = downarrow y by A8, Def16;
then  (DownMap I) . x c= (DownMap I) . y by A1, A9, WAYBEL_0:21;
hence  for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (DownMap I) . x or not b2 = (DownMap I) . y or b1 <= b2 ) by YELLOW_1:3; ::_thesis: verum
end;
end;
end;

Lm10:  for L being Semilattice
for x being Element of L
for I being Ideal of L holds (DownMap I) . x c= downarrow x
proof
let L be Semilattice; ::_thesis: for x being Element of L
for I being Ideal of L holds (DownMap I) . x c= downarrow x
let x be Element of L; ::_thesis: for I being Ideal of L holds (DownMap I) . x c= downarrow x
let I be Ideal of L; ::_thesis: (DownMap I) . x c= downarrow x
percases ( x <= sup I or not x <= sup I ) ;
suppose x <= sup I ; ::_thesis: (DownMap I) . x c= downarrow x
then  (DownMap I) . x = (downarrow x) /\ I by Def16;
hence  (DownMap I) . x c= downarrow x by XBOOLE_1:17; ::_thesis: verum
end;
suppose not x <= sup I ; ::_thesis: (DownMap I) . x c= downarrow x
hence  (DownMap I) . x c= downarrow x by Def16; ::_thesis: verum
end;
end;
end;

theorem Th35: :: WAYBEL_4:35
for L being Semilattice
for I being Ideal of L holds DownMap I in the carrier of (MonSet L)
proof
let L be Semilattice; ::_thesis: for I being Ideal of L holds DownMap I in the carrier of (MonSet L)
let I be Ideal of L; ::_thesis: DownMap I in the carrier of (MonSet L)
reconsider mI = DownMap I as Function of L,(InclPoset (Ids L)) ;
 ex s being Function of L,(InclPoset (Ids L)) st
( mI = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) )
proof
take  mI ; ::_thesis: ( mI = mI & mI is monotone & ( for x being Element of L holds mI . x c= downarrow x ) )
thus  ( mI = mI & mI is monotone & ( for x being Element of L holds mI . x c= downarrow x ) ) by Lm9, Lm10; ::_thesis: verum
end;
hence  DownMap I in the carrier of (MonSet L) by Def13; ::_thesis: verum
end;

theorem Th36: :: WAYBEL_4:36
for L being reflexive antisymmetric with_infima RelStr
for x being Element of L
for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for x being Element of L
for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D
let x be Element of L; ::_thesis: for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D
let D be non empty lower Subset of L; ::_thesis: {x} "/\" D = (downarrow x) /\ D
A1: {x} "/\" D =  {  (x9 "/\" y) where x9, y is Element of L : ( x9 in {x} & y in D )  }  by YELLOW_4:def_4;
thus  {x} "/\" D c= (downarrow x) /\ D :: according to XBOOLE_0:def_10 ::_thesis: (downarrow x) /\ D c= {x} "/\" D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} "/\" D or a in (downarrow x) /\ D )
assume  a in {x} "/\" D ; ::_thesis: a in (downarrow x) /\ D
then  a in  {  (x9 "/\" y) where x9, y is Element of L : ( x9 in {x} & y in D )  }  by YELLOW_4:def_4;
then consider x9, y being Element of L such that
A2: a = x9 "/\" y and
A3: x9 in {x} and
A4: y in D ;
reconsider a9 = a as Element of L by A2;
A5: x9 = x by A3, TARSKI:def_1;
A6: ex v being Element of L st
( x9 >= v & y >= v & ( for c being Element of L st x9 >= c & y >= c holds
v >= c ) ) by LATTICE3:def_11;
then A7: x9 "/\" y <= x9 by LATTICE3:def_14;
A8: x9 "/\" y <= y by A6, LATTICE3:def_14;
A9: a in downarrow x by A2, A5, A7, WAYBEL_0:17;
 a9 in D by A2, A4, A8, WAYBEL_0:def_19;
hence  a in (downarrow x) /\ D by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  (downarrow x) /\ D c= {x} "/\" D ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (downarrow x) /\ D or a in {x} "/\" D )
assume A10: a in (downarrow x) /\ D ; ::_thesis: a in {x} "/\" D
then A11: a in downarrow x by XBOOLE_0:def_4;
reconsider a9 = a as Element of D by A10, XBOOLE_0:def_4;
A12: x in {x} by TARSKI:def_1;
 a9 <= x by A11, WAYBEL_0:17;
then  a9 = a9 "/\" x by YELLOW_0:25;
hence  a in {x} "/\" D by A1, A12; ::_thesis: verum
end;
end;

begin

definition
let L be non empty RelStr ;
let AR be Relation of L;
attrAR is approximating  means :Def17: :: WAYBEL_4:def 17
 for x being Element of L holds x = sup (AR -below x);
end;

:: deftheorem Def17 defines approximating WAYBEL_4:def_17_:_
 for L being non empty RelStr
for AR being Relation of L holds
( AR is approximating iff for x being Element of L holds x = sup (AR -below x) );

definition
let L be non empty Poset;
let mp be Function of L,(InclPoset (Ids L));
attrmp is approximating  means :Def18: :: WAYBEL_4:def 18
 for x being Element of L ex ii being Subset of L st
( ii = mp . x & x = sup ii );
end;

:: deftheorem Def18 defines approximating WAYBEL_4:def_18_:_
 for L being non empty Poset
for mp being Function of L,(InclPoset (Ids L)) holds
( mp is approximating iff for x being Element of L ex ii being Subset of L st
( ii = mp . x & x = sup ii ) );

theorem Th37: :: WAYBEL_4:37
for L being lower-bounded meet-continuous Semilattice
for I being Ideal of L holds DownMap I is approximating
proof
let L be lower-bounded meet-continuous Semilattice; ::_thesis: for I being Ideal of L holds DownMap I is approximating
let I be Ideal of L; ::_thesis: DownMap I is approximating
 for x being Element of L ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii )
proof
let x be Element of L; ::_thesis: ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii )
set ii = (DownMap I) . x;
 (DownMap I) . x in the carrier of (InclPoset (Ids L)) ;
then  (DownMap I) . x in Ids L by YELLOW_1:1;
then consider ii9 being Ideal of L such that
A1: ii9 = (DownMap I) . x ;
reconsider dI = (downarrow x) /\ I as Subset of L ;
percases ( x <= sup I or not x <= sup I ) ;
supposeA2: x <= sup I ; ::_thesis: ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii )
then  sup ii9 = sup dI by A1, Def16
.= sup ({x} "/\" I) by Th36
.= x "/\" (sup I) by WAYBEL_2:def_6
.= x by A2, YELLOW_0:25 ;
hence  ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii ) by A1; ::_thesis: verum
end;
suppose not x <= sup I ; ::_thesis: ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii )
then  sup ii9 = sup (downarrow x) by A1, Def16
.= x by WAYBEL_0:34 ;
hence  ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii ) by A1; ::_thesis: verum
end;
end;
end;
hence  DownMap I is approximating by Def18; ::_thesis: verum
end;

Lm11:  for L being complete LATTICE
for x being Element of L
for D being directed Subset of L holds sup ({x} "/\" D) <= x
proof
let L be complete LATTICE; ::_thesis: for x being Element of L
for D being directed Subset of L holds sup ({x} "/\" D) <= x
let x be Element of L; ::_thesis: for D being directed Subset of L holds sup ({x} "/\" D) <= x
let D be directed Subset of L; ::_thesis: sup ({x} "/\" D) <= x
A1: {x} "/\" D =  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in D )  }  by YELLOW_4:def_4;
A2: ex_sup_of {x} "/\" D,L by YELLOW_0:17;
 for c being Element of L st c in {x} "/\" D holds
c <= x
proof
let c be Element of L; ::_thesis: ( c in {x} "/\" D implies c <= x )
assume  c in {x} "/\" D ; ::_thesis: c <= x
then consider a, b being Element of L such that
A3: c = a "/\" b and
A4: a in {x} and
 b in D by A1;
 a = x by A4, TARSKI:def_1;
hence  c <= x by A3, YELLOW_0:23; ::_thesis: verum
end;
then  x is_>=_than {x} "/\" D by LATTICE3:def_9;
hence  sup ({x} "/\" D) <= x by A2, YELLOW_0:30; ::_thesis: verum
end;

theorem Th38: :: WAYBEL_4:38
for L being lower-bounded continuous LATTICE holds L is meet-continuous
proof
let L be lower-bounded continuous LATTICE; ::_thesis: L is meet-continuous
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_L
for_x_being_Element_of_L_st_x_<=_sup_D_holds_
x_=_sup_({x}_"/\"_D)
let D be non empty directed Subset of L; ::_thesis: for x being Element of L st x <= sup D holds
x = sup ({x} "/\" D)
let x be Element of L; ::_thesis: ( x <= sup D implies x = sup ({x} "/\" D) )
assume A1: x <= sup D ; ::_thesis: x = sup ({x} "/\" D)
A2: ex_sup_of waybelow x,L by YELLOW_0:17;
A3: ex_sup_of downarrow (sup ({x} "/\" D)),L by YELLOW_0:17;
 waybelow x c= downarrow (sup ({x} "/\" D))
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in waybelow x or q in downarrow (sup ({x} "/\" D)) )
assume  q in waybelow x ; ::_thesis: q in downarrow (sup ({x} "/\" D))
then  q in  {  y where y is Element of L : y << x  }  by WAYBEL_3:def_3;
then consider q9 being Element of L such that
A4: q9 = q and
A5: q9 << x ;
A6: q9 <= x by A5, WAYBEL_3:1;
consider d being Element of L such that
A7: d in D and
A8: q9 <= d by A1, A5, WAYBEL_3:def_1;
 x in {x} by TARSKI:def_1;
then  x "/\" d in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in D )  }  by A7;
then A9: x "/\" d in {x} "/\" D by YELLOW_4:def_4;
 ex_inf_of {x,d},L by YELLOW_0:17;
then A10: q9 <= x "/\" d by A6, A8, YELLOW_0:19;
 sup ({x} "/\" D) is_>=_than {x} "/\" D by YELLOW_0:32;
then  x "/\" d <= sup ({x} "/\" D) by A9, LATTICE3:def_9;
then  q9 <= sup ({x} "/\" D) by A10, ORDERS_2:3;
hence  q in downarrow (sup ({x} "/\" D)) by A4, WAYBEL_0:17; ::_thesis: verum
end;
then  sup (waybelow x) <= sup (downarrow (sup ({x} "/\" D))) by A2, A3, YELLOW_0:34;
then  sup (waybelow x) <= sup ({x} "/\" D) by WAYBEL_0:34;
then A11: x <= sup ({x} "/\" D) by WAYBEL_3:def_5;
 sup ({x} "/\" D) <= x by Lm11;
hence  x = sup ({x} "/\" D) by A11, ORDERS_2:2; ::_thesis: verum
end;
then  for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) ;
hence  L is meet-continuous by WAYBEL_2:52; ::_thesis: verum
end;

registration
cluster reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous  ->  lower-bounded meet-continuous for RelStr ;
coherence
 for b1 being lower-bounded LATTICE st b1 is continuous holds
b1 is meet-continuous by Th38;
end;

theorem :: WAYBEL_4:39
for L being lower-bounded continuous LATTICE
for I being Ideal of L holds DownMap I is approximating by Th37;

registration
let L be non empty reflexive antisymmetric RelStr ;
clusterL -waybelow  ->  auxiliary(i) ;
coherence
 L -waybelow is auxiliary(i)
proof
let x, y be Element of L; :: according to WAYBEL_4:def_3 ::_thesis: ( [x,y] in L -waybelow implies x <= y )
assume  [x,y] in L -waybelow ; ::_thesis: x <= y
then  x << y by Def1;
hence  x <= y by WAYBEL_3:1; ::_thesis: verum
end;
end;

registration
let L be non empty reflexive transitive RelStr ;
clusterL -waybelow  ->  auxiliary(ii) ;
coherence
 L -waybelow is auxiliary(ii)
proof
set AR = L -waybelow ;
let x, y, z, u be Element of L; :: according to WAYBEL_4:def_4 ::_thesis: ( u <= x & [x,y] in L -waybelow & y <= z implies [u,z] in L -waybelow )
assume that
A1: u <= x and
A2: [x,y] in L -waybelow and
A3: y <= z ; ::_thesis: [u,z] in L -waybelow
 x << y by A2, Def1;
then  u << z by A1, A3, WAYBEL_3:2;
hence  [u,z] in L -waybelow by Def1; ::_thesis: verum
end;
end;

registration
let L be with_suprema Poset;
clusterL -waybelow  ->  auxiliary(iii) ;
coherence
 L -waybelow is auxiliary(iii)
proof
set AR = L -waybelow ;
let x, y, z be Element of L; :: according to WAYBEL_4:def_5 ::_thesis: ( [x,z] in L -waybelow & [y,z] in L -waybelow implies [(x "\/" y),z] in L -waybelow )
assume that
A1: [x,z] in L -waybelow and
A2: [y,z] in L -waybelow ; ::_thesis: [(x "\/" y),z] in L -waybelow
A3: x << z by A1, Def1;
 y << z by A2, Def1;
then  x "\/" y << z by A3, WAYBEL_3:3;
hence  [(x "\/" y),z] in L -waybelow by Def1; ::_thesis: verum
end;
end;

registration
let L be non empty /\-complete Poset;
clusterL -waybelow  ->  auxiliary(iii) ;
coherence
 L -waybelow is auxiliary(iii)
proof
set AR = L -waybelow ;
let x, y, z be Element of L; :: according to WAYBEL_4:def_5 ::_thesis: ( [x,z] in L -waybelow & [y,z] in L -waybelow implies [(x "\/" y),z] in L -waybelow )
assume that
A1: [x,z] in L -waybelow and
A2: [y,z] in L -waybelow ; ::_thesis: [(x "\/" y),z] in L -waybelow
A3: x << z by A1, Def1;
 y << z by A2, Def1;
then  x "\/" y << z by A3, WAYBEL_3:3;
hence  [(x "\/" y),z] in L -waybelow by Def1; ::_thesis: verum
end;
end;

registration
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
clusterL -waybelow  ->  auxiliary(iv) ;
coherence
 L -waybelow is auxiliary(iv)
proof
let x be Element of L; :: according to WAYBEL_4:def_6 ::_thesis: [(Bottom L),x] in L -waybelow
 Bottom L << x by WAYBEL_3:4;
hence  [(Bottom L),x] in L -waybelow by Def1; ::_thesis: verum
end;
end;

theorem Th40: :: WAYBEL_4:40
for L being complete LATTICE
for x being Element of L holds (L -waybelow) -below x = waybelow x
proof
let L be complete LATTICE; ::_thesis: for x being Element of L holds (L -waybelow) -below x = waybelow x
let x be Element of L; ::_thesis: (L -waybelow) -below x = waybelow x
set AR = L -waybelow ;
set A =  {  y where y is Element of L : [y,x] in L -waybelow  }  ;
set B =  {  y where y is Element of L : y << x  }  ;
A1:  {  y where y is Element of L : [y,x] in L -waybelow  }  c=  {  y where y is Element of L : y << x  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  y where y is Element of L : [y,x] in L -waybelow  }  or a in  {  y where y is Element of L : y << x  }  )
assume  a in  {  y where y is Element of L : [y,x] in L -waybelow  }  ; ::_thesis: a in  {  y where y is Element of L : y << x  }
then consider v being Element of L such that
A2: a = v and
A3: [v,x] in L -waybelow ;
 v << x by A3, Def1;
hence  a in  {  y where y is Element of L : y << x  }  by A2; ::_thesis: verum
end;
  {  y where y is Element of L : y << x  }  c=  {  y where y is Element of L : [y,x] in L -waybelow  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  y where y is Element of L : y << x  }  or a in  {  y where y is Element of L : [y,x] in L -waybelow  }  )
assume  a in  {  y where y is Element of L : y << x  }  ; ::_thesis: a in  {  y where y is Element of L : [y,x] in L -waybelow  }
then consider v being Element of L such that
A4: a = v and
A5: v << x ;
 [v,x] in L -waybelow by A5, Def1;
hence  a in  {  y where y is Element of L : [y,x] in L -waybelow  }  by A4; ::_thesis: verum
end;
then   {  y where y is Element of L : [y,x] in L -waybelow  }  =  {  y where y is Element of L : y << x  }  by A1, XBOOLE_0:def_10;
hence  (L -waybelow) -below x = waybelow x by WAYBEL_3:def_3; ::_thesis: verum
end;

theorem Th41: :: WAYBEL_4:41
for L being LATTICE holds IntRel L is approximating
proof
let L be LATTICE; ::_thesis: IntRel L is approximating
set AR = IntRel L;
let x be Element of L; :: according to WAYBEL_4:def_17 ::_thesis: x = sup ((IntRel L) -below x)
set A =  {  y where y is Element of L : [y,x] in IntRel L  }  ;
set E =  {  u where u is Element of L : u <= x  }  ;
A1:  {  y where y is Element of L : [y,x] in IntRel L  }  c=  {  u where u is Element of L : u <= x  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  y where y is Element of L : [y,x] in IntRel L  }  or a in  {  u where u is Element of L : u <= x  }  )
assume  a in  {  y where y is Element of L : [y,x] in IntRel L  }  ; ::_thesis: a in  {  u where u is Element of L : u <= x  }
then consider v being Element of L such that
A2: a = v and
A3: [v,x] in IntRel L ;
 v <= x by A3, ORDERS_2:def_5;
hence  a in  {  u where u is Element of L : u <= x  }  by A2; ::_thesis: verum
end;
  {  u where u is Element of L : u <= x  }  c=  {  y where y is Element of L : [y,x] in IntRel L  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  u where u is Element of L : u <= x  }  or a in  {  y where y is Element of L : [y,x] in IntRel L  }  )
assume  a in  {  u where u is Element of L : u <= x  }  ; ::_thesis: a in  {  y where y is Element of L : [y,x] in IntRel L  }
then consider v being Element of L such that
A4: a = v and
A5: v <= x ;
 [v,x] in IntRel L by A5, ORDERS_2:def_5;
hence  a in  {  y where y is Element of L : [y,x] in IntRel L  }  by A4; ::_thesis: verum
end;
then A6:  {  y where y is Element of L : [y,x] in IntRel L  }  =  {  u where u is Element of L : u <= x  }  by A1, XBOOLE_0:def_10;
  {  y where y is Element of L : y <= x  }  c= the carrier of L
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  y where y is Element of L : y <= x  }  or z in the carrier of L )
assume  z in  {  y where y is Element of L : y <= x  }  ; ::_thesis: z in the carrier of L
then  ex y being Element of L st
( z = y & y <= x ) ;
hence  z in the carrier of L ; ::_thesis: verum
end;
then reconsider E =  {  u where u is Element of L : u <= x  }  as Subset of L ;
A7: x is_>=_than E
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in E or b <= x )
assume  b in E ; ::_thesis: b <= x
then  ex b9 being Element of L st
( b9 = b & b9 <= x ) ;
hence  b <= x ; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_L_st_b_is_>=_than_E_holds_
x_<=_b
let b be Element of L; ::_thesis: ( b is_>=_than E implies x <= b )
assume A8: b is_>=_than E ; ::_thesis: x <= b
 x in E ;
hence  x <= b by A8, LATTICE3:def_9; ::_thesis: verum
end;
hence  x = sup ((IntRel L) -below x) by A6, A7, YELLOW_0:30; ::_thesis: verum
end;

Lm12:  for L being lower-bounded continuous LATTICE holds L -waybelow is approximating
proof
let L be lower-bounded continuous LATTICE; ::_thesis: L -waybelow is approximating
let x be Element of L; :: according to WAYBEL_4:def_17 ::_thesis: x = sup ((L -waybelow) -below x)
 x = sup (waybelow x) by WAYBEL_3:def_5;
hence  x = sup ((L -waybelow) -below x) by Th40; ::_thesis: verum
end;

registration
let L be lower-bounded continuous LATTICE;
clusterL -waybelow  ->  approximating ;
coherence
 L -waybelow is approximating by Lm12;
end;

registration
let L be complete LATTICE;
cluster Relation-like auxiliary approximating for Element of bool [: the carrier of L, the carrier of L:];
existence
 ex b1 being Relation of L st
( b1 is approximating & b1 is auxiliary )
proof
reconsider A = IntRel L as auxiliary Relation of L ;
 A is approximating by Th41;
hence  ex b1 being Relation of L st
( b1 is approximating & b1 is auxiliary ) ; ::_thesis: verum
end;
end;

definition
let L be complete LATTICE;
defpred S1[ set ] means $1 is auxiliary approximating Relation of L;
func App L ->  set  means :Def19: :: WAYBEL_4:def 19
 for a being set holds
( a in it iff a is auxiliary approximating Relation of L );
existence
 ex b1 being set st
for a being set holds
( a in b1 iff a is auxiliary approximating Relation of L )
proof
consider X being set  such that
A1: for a being set holds
( a in X iff ( a in Aux L & S1[a] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for a being set holds
( a in X iff a is auxiliary approximating Relation of L )
 for a being set st a is auxiliary approximating Relation of L holds
a in X
proof
let a be set ; ::_thesis: ( a is auxiliary approximating Relation of L implies a in X )
assume A2: a is auxiliary approximating Relation of L ; ::_thesis: a in X
then  a in Aux L by Def8;
hence  a in X by A1, A2; ::_thesis: verum
end;
hence  for a being set holds
( a in X iff a is auxiliary approximating Relation of L ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for a being set holds
( a in b1 iff a is auxiliary approximating Relation of L ) ) & ( for a being set holds
( a in b2 iff a is auxiliary approximating Relation of L ) ) holds
b1 = b2
proof
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def19 defines App WAYBEL_4:def_19_:_
 for L being complete LATTICE
for b2 being set holds
( b2 = App L iff for a being set holds
( a in b2 iff a is auxiliary approximating Relation of L ) );

registration
let L be complete LATTICE;
cluster App L ->  non empty ;
coherence
 not App L is empty
proof
set a = the auxiliary approximating Relation of L;
 the auxiliary approximating Relation of L in App L by Def19;
hence  not App L is empty ; ::_thesis: verum
end;
end;

theorem Th42: :: WAYBEL_4:42
for L being complete LATTICE
for mp being Function of L,(InclPoset (Ids L)) st mp is approximating & mp in the carrier of (MonSet L) holds
ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp
proof
let L be complete LATTICE; ::_thesis: for mp being Function of L,(InclPoset (Ids L)) st mp is approximating & mp in the carrier of (MonSet L) holds
ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp
let mp be Function of L,(InclPoset (Ids L)); ::_thesis: ( mp is approximating & mp in the carrier of (MonSet L) implies ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp )
assume that
A1: mp is approximating and
A2: mp in the carrier of (MonSet L) ; ::_thesis: ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp
consider AR being auxiliary Relation of L such that
A3: AR = (Map2Rel L) . mp and
A4: for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = mp & x9 in s9 . y9 ) ) by A2, Def15;
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(AR_-below_x)
let x be Element of L; ::_thesis: x = sup (AR -below x)
A5: ex ii being Subset of L st
( ii = mp . x & x = sup ii ) by A1, Def18;
A6: AR -below x c= mp . x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in AR -below x or a in mp . x )
assume  a in AR -below x ; ::_thesis: a in mp . x
then  [a,x] in AR by Th13;
then  ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a & y9 = x & s9 = mp & x9 in s9 . y9 ) by A4;
hence  a in mp . x ; ::_thesis: verum
end;
 mp . x c= AR -below x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in mp . x or a in AR -below x )
assume A7: a in mp . x ; ::_thesis: a in AR -below x
then reconsider a9 = a as Element of L by A5;
 [a9,x] in AR by A4, A7;
hence  a in AR -below x ; ::_thesis: verum
end;
hence  x = sup (AR -below x) by A5, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
then reconsider AR = AR as auxiliary approximating Relation of L by Def17;
take  AR ; ::_thesis: AR = (Map2Rel L) . mp
thus  AR = (Map2Rel L) . mp by A3; ::_thesis: verum
end;

theorem Th43: :: WAYBEL_4:43
for L being complete LATTICE
for x being Element of L holds meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = waybelow x
proof
let L be complete LATTICE; ::_thesis: for x being Element of L holds meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = waybelow x
let x be Element of L; ::_thesis: meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = waybelow x
set A =  {  ((DownMap I) . x) where I is Ideal of L : verum  }  ;
set A1 =  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  ;
A1:  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c=  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  or a in  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }  )
assume  a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }
then consider I1 being Ideal of L such that
A2: a = (DownMap I1) . x and
A3: x <= sup I1 ;
 a = (downarrow x) /\ I1 by A2, A3, Def16;
hence  a in  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }  by A3; ::_thesis: verum
end;
  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }  c=  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }  or a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  )
assume  a in  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }
then consider I1 being Ideal of L such that
A4: a = (downarrow x) /\ I1 and
A5: x <= sup I1 ;
 a = (DownMap I1) . x by A4, A5, Def16;
hence  a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A5; ::_thesis: verum
end;
then A6:  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  =  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }  by A1, XBOOLE_0:def_10;
set A2 =  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  ;
A7:  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  c=  {  (downarrow x) where I is Ideal of L : not x <= sup I  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  or a in  {  (downarrow x) where I is Ideal of L : not x <= sup I  }  )
assume  a in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  ; ::_thesis: a in  {  (downarrow x) where I is Ideal of L : not x <= sup I  }
then A8: ex I1 being Ideal of L st
( a = (DownMap I1) . x & not x <= sup I1 ) ;
then  a = downarrow x by Def16;
hence  a in  {  (downarrow x) where I is Ideal of L : not x <= sup I  }  by A8; ::_thesis: verum
end;
  {  (downarrow x) where I is Ideal of L : not x <= sup I  }  c=  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (downarrow x) where I is Ideal of L : not x <= sup I  }  or a in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  )
assume  a in  {  (downarrow x) where I is Ideal of L : not x <= sup I  }  ; ::_thesis: a in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }
then consider I1 being Ideal of L such that
A9: a = downarrow x and
A10: not x <= sup I1 ;
 a = (DownMap I1) . x by A9, A10, Def16;
hence  a in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  by A10; ::_thesis: verum
end;
then A11:  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  =  {  (downarrow x) where I is Ideal of L : not x <= sup I  }  by A7, XBOOLE_0:def_10;
A12:  {  ((DownMap I) . x) where I is Ideal of L : verum  }  c=  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  \/  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }  or a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  \/  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  )
assume  a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }  ; ::_thesis: a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  \/  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }
then consider I2 being Ideal of L such that
A13: a = (DownMap I2) . x ;
 ( x <= sup I2 or not x <= sup I2 ) ;
then  ( a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  or a in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  ) by A13;
hence  a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  \/  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  by XBOOLE_0:def_3; ::_thesis: verum
end;
  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  \/  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  c=  {  ((DownMap I) . x) where I is Ideal of L : verum  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  \/  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  or a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }  )
assume  a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  \/  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  ; ::_thesis: a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }
then  ( a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  or a in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  ) by XBOOLE_0:def_3;
then consider I2, I3 being Ideal of L such that
A14: ( ( a = (DownMap I2) . x & x <= sup I2 ) or ( a = (DownMap I3) . x & not x <= sup I3 ) ) ;
percases ( ( a = (DownMap I2) . x & x <= sup I2 ) or ( a = (DownMap I3) . x & not x <= sup I3 ) ) by A14;
suppose ( a = (DownMap I2) . x & x <= sup I2 ) ; ::_thesis: a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }
hence  a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }  ; ::_thesis: verum
end;
suppose ( a = (DownMap I3) . x & not x <= sup I3 ) ; ::_thesis: a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }
hence  a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }  ; ::_thesis: verum
end;
end;
end;
then A15:  {  ((DownMap I) . x) where I is Ideal of L : verum  }  =  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  \/  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  by A12, XBOOLE_0:def_10;
percases ( x = Bottom L or Bottom L <> x ) ;
supposeA16: x = Bottom L ; ::_thesis: meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = waybelow x
A17:  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  = {}
proof
assume   {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  <> {} ; ::_thesis: contradiction
then reconsider A29 =  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  as non empty set ;
set a = the Element of A29;
 the Element of A29 in A29 ;
then  ex I1 being Ideal of L st
( the Element of A29 = downarrow x & not x <= sup I1 ) by A11;
hence  contradiction by A16, YELLOW_0:44; ::_thesis: verum
end;
set Dx = downarrow x;
 x <= sup (downarrow x) by A16, YELLOW_0:44;
then A18: (downarrow x) /\ (downarrow x) in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A6;
  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c=  {  K where K is Ideal of L : x <= sup K  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  or a in  {  K where K is Ideal of L : x <= sup K  }  )
assume  a in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in  {  K where K is Ideal of L : x <= sup K  }
then  ex H being Ideal of L st
( a = (downarrow x) /\ H & x <= sup H ) by A6;
then reconsider a9 = a as Ideal of L by YELLOW_2:40;
 x <= sup a9 by A16, YELLOW_0:44;
hence  a in  {  K where K is Ideal of L : x <= sup K  }  ; ::_thesis: verum
end;
then A19: meet  {  K where K is Ideal of L : x <= sup K  }  c= meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A18, SETFAM_1:6;
A20: meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  = {x}
proof
reconsider I9 = downarrow x as Ideal of L ;
 x <= sup I9 by A16, YELLOW_0:44;
then  (downarrow x) /\ I9 in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A6;
then  {x} in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A16, Th23;
hence  meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c= {x} by SETFAM_1:3; :: according to XBOOLE_0:def_10 ::_thesis: {x} c= meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }
 for Z1 being set st Z1 in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  holds
{x} c= Z1
proof
let Z1 be set ; ::_thesis: ( Z1 in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  implies {x} c= Z1 )
assume  Z1 in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  ; ::_thesis: {x} c= Z1
then consider Z19 being Ideal of L such that
A21: Z1 = (downarrow x) /\ Z19 and
 x <= sup Z19 by A6;
A22: {x} c= Z19 by A16, Lm4;
 {x} c= downarrow x by A16, Th23;
hence  {x} c= Z1 by A21, A22, XBOOLE_1:19; ::_thesis: verum
end;
hence  {x} c= meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A18, SETFAM_1:5; ::_thesis: verum
end;
set E = the Ideal of L;
 x <= sup the Ideal of L by A16, YELLOW_0:44;
then A23: the Ideal of L in  {  K where K is Ideal of L : x <= sup K  }  ;
 for Z1 being set st Z1 in  {  K where K is Ideal of L : x <= sup K  }  holds
meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c= Z1
proof
let Z1 be set ; ::_thesis: ( Z1 in  {  K where K is Ideal of L : x <= sup K  }  implies meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c= Z1 )
assume  Z1 in  {  K where K is Ideal of L : x <= sup K  }  ; ::_thesis: meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c= Z1
then  ex K1 being Ideal of L st
( K1 = Z1 & x <= sup K1 ) ;
hence  meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c= Z1 by A16, A20, Lm4; ::_thesis: verum
end;
then  meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c= meet  {  K where K is Ideal of L : x <= sup K  }  by A23, SETFAM_1:5;
then  meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  = meet  {  K where K is Ideal of L : x <= sup K  }  by A19, XBOOLE_0:def_10;
hence  meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = waybelow x by A15, A17, Th34; ::_thesis: verum
end;
supposeA24: Bottom L <> x ; ::_thesis: meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = waybelow x
set O = downarrow (Bottom L);
A25: sup (downarrow (Bottom L)) = Bottom L by WAYBEL_0:34;
then  not x < sup (downarrow (Bottom L)) by ORDERS_2:6, YELLOW_0:44;
then  not x <= sup (downarrow (Bottom L)) by A24, A25, ORDERS_2:def_6;
then A26: downarrow x in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  by A11;
reconsider O1 = downarrow x as Ideal of L ;
A27: x <= sup O1 by WAYBEL_0:34;
 downarrow x = (downarrow x) /\ O1 ;
then A28: downarrow x in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A6, A27;
A29: meet  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  c= downarrow x by A26, SETFAM_1:3;
now__::_thesis:_for_Z1_being_set_st_Z1_in__{__((DownMap_I)_._x)_where_I_is_Ideal_of_L_:_not_x_<=_sup_I__}__holds_
downarrow_x_c=_Z1
let Z1 be set ; ::_thesis: ( Z1 in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  implies downarrow x c= Z1 )
assume  Z1 in  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  ; ::_thesis: downarrow x c= Z1
then  ex L1 being Ideal of L st
( Z1 = downarrow x & not x <= sup L1 ) by A11;
hence  downarrow x c= Z1 ; ::_thesis: verum
end;
then  downarrow x c= meet  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  by A26, SETFAM_1:5;
then A30: meet  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  = downarrow x by A29, XBOOLE_0:def_10;
A31: meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = (meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  ) /\ (meet  {  ((DownMap I) . x) where I is Ideal of L : not x <= sup I  }  ) by A15, A26, A28, SETFAM_1:9;
A32: meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c= downarrow x by A28, SETFAM_1:3;
A33: meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A28, A30, A31, SETFAM_1:3, XBOOLE_1:28;
A34: meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  c= (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  )
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  or a in (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  ) )
assume A35: a in meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  )
thus  a in (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  ) ::_thesis: verum
proof
reconsider L9 = [#] L as Subset of L ;
 ex_sup_of L9,L by YELLOW_0:17;
then  L9 is_<=_than sup L9 by YELLOW_0:def_9;
then  x <= sup L9 by LATTICE3:def_9;
then A36: L9 in  {  I where I is Ideal of L : x <= sup I  }  ;
now__::_thesis:_for_Y1_being_set_st_Y1_in__{__I_where_I_is_Ideal_of_L_:_x_<=_sup_I__}__holds_
a_in_Y1
let Y1 be set ; ::_thesis: ( Y1 in  {  I where I is Ideal of L : x <= sup I  }  implies a in Y1 )
assume  Y1 in  {  I where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in Y1
then consider Y19 being Ideal of L such that
A37: Y1 = Y19 and
A38: x <= sup Y19 ;
A39: (downarrow x) /\ Y19 c= Y19 by XBOOLE_1:17;
 (downarrow x) /\ Y19 in  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A6, A38;
then  a in (downarrow x) /\ Y19 by A35, SETFAM_1:def_1;
hence  a in Y1 by A37, A39; ::_thesis: verum
end;
then  a in meet  {  I where I is Ideal of L : x <= sup I  }  by A36, SETFAM_1:def_1;
hence  a in (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  ) by A32, A35, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
 (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  ) c= meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  ) or a in meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  )
assume A40: a in (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  ) ; ::_thesis: a in meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }
then A41: a in downarrow x by XBOOLE_0:def_4;
A42: a in meet  {  I where I is Ideal of L : x <= sup I  }  by A40, XBOOLE_0:def_4;
now__::_thesis:_for_Y1_being_set_st_Y1_in__{__((downarrow_x)_/\_I)_where_I_is_Ideal_of_L_:_x_<=_sup_I__}__holds_
a_in_Y1
let Y1 be set ; ::_thesis: ( Y1 in  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }  implies a in Y1 )
assume  Y1 in  {  ((downarrow x) /\ I) where I is Ideal of L : x <= sup I  }  ; ::_thesis: a in Y1
then consider I1 being Ideal of L such that
A43: Y1 = (downarrow x) /\ I1 and
A44: x <= sup I1 ;
 I1 in  {  I where I is Ideal of L : x <= sup I  }  by A44;
then  a in I1 by A42, SETFAM_1:def_1;
hence  a in Y1 by A41, A43, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  a in meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A6, A28, SETFAM_1:def_1; ::_thesis: verum
end;
then  (downarrow x) /\ (meet  {  I where I is Ideal of L : x <= sup I  }  ) = meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by A34, XBOOLE_0:def_10;
then  (downarrow x) /\ (waybelow x) = meet  {  ((DownMap I) . x) where I is Ideal of L : x <= sup I  }  by Th34;
hence  meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = waybelow x by A33, WAYBEL_3:11, XBOOLE_1:28; ::_thesis: verum
end;
end;
end;

theorem Th44: :: WAYBEL_4:44
for L being lower-bounded meet-continuous LATTICE
for x being Element of L holds meet  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  = waybelow x
proof
let L be lower-bounded meet-continuous LATTICE; ::_thesis: for x being Element of L holds meet  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  = waybelow x
let x be Element of L; ::_thesis: meet  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  = waybelow x
set A =  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  ;
set AA = the auxiliary approximating Relation of L;
 the auxiliary approximating Relation of L in App L by Def19;
then A1: the auxiliary approximating Relation of L -below x in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  ;
A2: meet  {  I where I is Ideal of L : x <= sup I  }  = waybelow x by Th34;
A3: meet  {  ((DownMap I) . x) where I is Ideal of L : verum  }  = waybelow x by Th43;
set I1 = the Ideal of L;
A4: (DownMap the Ideal of L) . x in  {  ((DownMap I) . x) where I is Ideal of L : verum  }  ;
  {  ((DownMap I) . x) where I is Ideal of L : verum  }  c=  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }  or a in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  )
assume  a in  {  ((DownMap I) . x) where I is Ideal of L : verum  }  ; ::_thesis: a in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }
then consider I being Ideal of L such that
A5: a = (DownMap I) . x ;
A6: DownMap I is approximating by Th37;
 DownMap I in the carrier of (MonSet L) by Th35;
then consider AR being auxiliary Relation of L such that
A7: AR = (Map2Rel L) . (DownMap I) and
A8: for x, y being set holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = DownMap I & x9 in s9 . y9 ) ) by Def15;
A9: ex AR1 being auxiliary approximating Relation of L st AR1 = (Map2Rel L) . (DownMap I) by A6, Th35, Th42;
A10: ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii ) by A6, Def18;
A11: AR -below x c= (DownMap I) . x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in AR -below x or a in (DownMap I) . x )
assume  a in AR -below x ; ::_thesis: a in (DownMap I) . x
then  [a,x] in AR by Th13;
then  ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a & y9 = x & s9 = DownMap I & x9 in s9 . y9 ) by A8;
hence  a in (DownMap I) . x ; ::_thesis: verum
end;
 (DownMap I) . x c= AR -below x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (DownMap I) . x or a in AR -below x )
assume A12: a in (DownMap I) . x ; ::_thesis: a in AR -below x
then reconsider a9 = a as Element of L by A10;
 [a9,x] in AR by A8, A12;
hence  a in AR -below x ; ::_thesis: verum
end;
then A13: AR -below x = (DownMap I) . x by A11, XBOOLE_0:def_10;
 AR in App L by A7, A9, Def19;
hence  a in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  by A5, A13; ::_thesis: verum
end;
hence  meet  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  c= waybelow x by A3, A4, SETFAM_1:6; :: according to XBOOLE_0:def_10 ::_thesis: waybelow x c= meet  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }
  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  c=  {  I where I is Ideal of L : x <= sup I  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  or a in  {  I where I is Ideal of L : x <= sup I  }  )
assume  a in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  ; ::_thesis: a in  {  I where I is Ideal of L : x <= sup I  }
then consider AR being auxiliary Relation of L such that
A14: a = AR -below x and
A15: AR in App L ;
reconsider AR = AR as auxiliary approximating Relation of L by A15, Def19;
 sup (AR -below x) = x by Def17;
hence  a in  {  I where I is Ideal of L : x <= sup I  }  by A14; ::_thesis: verum
end;
hence  waybelow x c= meet  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  by A1, A2, SETFAM_1:6; ::_thesis: verum
end;

theorem Th45: :: WAYBEL_4:45
for L being complete LATTICE holds
( L is continuous iff for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) )
proof
let L be complete LATTICE; ::_thesis: ( L is continuous iff for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) )
set AR = L -waybelow ;
hereby  ::_thesis: ( ( for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) ) implies L is continuous )
assume A1: L is continuous ; ::_thesis: for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating )
then reconsider L9 = L as lower-bounded meet-continuous LATTICE ;
thus  for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) ::_thesis: verum
proof
let R be auxiliary approximating Relation of L; ::_thesis: ( L -waybelow c= R & L -waybelow is approximating )
reconsider R9 = R as auxiliary approximating Relation of L9 ;
 for a, b being set st [a,b] in L -waybelow holds
[a,b] in R
proof
let a, b be set ; ::_thesis: ( [a,b] in L -waybelow implies [a,b] in R )
assume A2: [a,b] in L -waybelow ; ::_thesis: [a,b] in R
then reconsider a9 = a, b9 = b as Element of L9 by ZFMISC_1:87;
 a9 << b9 by A2, Def1;
then A3: a9 in waybelow b9 by WAYBEL_3:7;
A4: meet  {  (A1 -below b9) where A1 is auxiliary Relation of L9 : A1 in App L9  }  = waybelow b9 by Th44;
 R9 in App L9 by Def19;
then  R9 -below b9 in  {  (A1 -below b9) where A1 is auxiliary Relation of L9 : A1 in App L9  }  ;
then  waybelow b9 c= R9 -below b9 by A4, SETFAM_1:3;
hence  [a,b] in R by A3, Th13; ::_thesis: verum
end;
hence  L -waybelow c= R by RELAT_1:def_3; ::_thesis: L -waybelow is approximating
thus  L -waybelow is approximating by A1; ::_thesis: verum
end;
end;
assume A5: for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) ; ::_thesis: L is continuous
 for x being Element of L holds x = sup (waybelow x)
proof
let x be Element of L; ::_thesis: x = sup (waybelow x)
 x = sup ((L -waybelow) -below x) by A5, Def17;
hence  x = sup (waybelow x) by Th40; ::_thesis: verum
end;
then  L is satisfying_axiom_of_approximation by WAYBEL_3:def_5;
hence  L is continuous ; ::_thesis: verum
end;

theorem :: WAYBEL_4:46
for L being complete LATTICE holds
( L is continuous iff ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 ) )
proof
let L be complete LATTICE; ::_thesis: ( L is continuous iff ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 ) )
hereby  ::_thesis: ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 implies L is continuous )
assume A1: L is continuous ; ::_thesis: ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 )
hence  L is meet-continuous ; ::_thesis: ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9
reconsider R = L -waybelow as auxiliary approximating Relation of L by A1;
take R = R; ::_thesis: for R9 being auxiliary approximating Relation of L holds R c= R9
thus  for R9 being auxiliary approximating Relation of L holds R c= R9 by A1, Th45; ::_thesis: verum
end;
assume A2: L is meet-continuous ; ::_thesis: ( for R being auxiliary approximating Relation of L holds
not for R9 being auxiliary approximating Relation of L holds R c= R9 or L is continuous )
given R being auxiliary approximating Relation of L such that A3: for R9 being auxiliary approximating Relation of L holds R c= R9 ; ::_thesis: L is continuous
 for x being Element of L holds x = sup (waybelow x)
proof
let x be Element of L; ::_thesis: x = sup (waybelow x)
set K =  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  ;
A4: meet  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  = waybelow x by A2, Th44;
 R in App L by Def19;
then A5: R -below x in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  ;
then A6: waybelow x c= R -below x by A4, SETFAM_1:3;
A7: sup (R -below x) = x by Def17;
 for a being set st a in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  holds
R -below x c= a
proof
let a be set ; ::_thesis: ( a in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  implies R -below x c= a )
assume  a in  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  ; ::_thesis: R -below x c= a
then consider AA being auxiliary Relation of L such that
A8: a = AA -below x and
A9: AA in App L ;
reconsider AA = AA as auxiliary approximating Relation of L by A9, Def19;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in R -below x or b in a )
assume A10: b in R -below x ; ::_thesis: b in a
 R -below x c= AA -below x by A3, Th29;
hence  b in a by A8, A10; ::_thesis: verum
end;
then  R -below x c= meet  {  (AR -below x) where AR is auxiliary Relation of L : AR in App L  }  by A5, SETFAM_1:5;
hence  x = sup (waybelow x) by A4, A6, A7, XBOOLE_0:def_10; ::_thesis: verum
end;
then  L is satisfying_axiom_of_approximation by WAYBEL_3:def_5;
hence  L is continuous ; ::_thesis: verum
end;

definition
let L be RelStr ;
let AR be Relation of L;
attrAR is satisfying_SI  means :Def20: :: WAYBEL_4:def 20
 for x, z being Element of L st [x,z] in AR & x <> z holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR & x <> y );
end;

:: deftheorem Def20 defines satisfying_SI WAYBEL_4:def_20_:_
 for L being RelStr
for AR being Relation of L holds
( AR is satisfying_SI iff for x, z being Element of L st [x,z] in AR & x <> z holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR & x <> y ) );

definition
let L be RelStr ;
let AR be Relation of L;
attrAR is satisfying_INT  means :Def21: :: WAYBEL_4:def 21
 for x, z being Element of L st [x,z] in AR holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR );
end;

:: deftheorem Def21 defines satisfying_INT WAYBEL_4:def_21_:_
 for L being RelStr
for AR being Relation of L holds
( AR is satisfying_INT iff for x, z being Element of L st [x,z] in AR holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) );

theorem Th47: :: WAYBEL_4:47
for L being RelStr
for AR being Relation of L st AR is satisfying_SI holds
AR is satisfying_INT
proof
let L be RelStr ; ::_thesis: for AR being Relation of L st AR is satisfying_SI holds
AR is satisfying_INT
let AR be Relation of L; ::_thesis: ( AR is satisfying_SI implies AR is satisfying_INT )
assume A1: AR is satisfying_SI ; ::_thesis: AR is satisfying_INT
let x, z be Element of L; :: according to WAYBEL_4:def_21 ::_thesis: ( [x,z] in AR implies ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) )
 ( [x,z] in AR implies ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) )
proof
assume A2: [x,z] in AR ; ::_thesis: ex y being Element of L st
( [x,y] in AR & [y,z] in AR )
percases ( x <> z or x = z ) ;
suppose x <> z ; ::_thesis: ex y being Element of L st
( [x,y] in AR & [y,z] in AR )
then  ex y being Element of L st
( [x,y] in AR & [y,z] in AR & x <> y ) by A1, A2, Def20;
hence  ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) ; ::_thesis: verum
end;
suppose x = z ; ::_thesis: ex y being Element of L st
( [x,y] in AR & [y,z] in AR )
hence  ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) by A2; ::_thesis: verum
end;
end;
end;
hence  ( [x,z] in AR implies ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) ) ; ::_thesis: verum
end;

registration
let L be non empty RelStr ;
cluster satisfying_SI  ->  satisfying_INT for Element of bool [: the carrier of L, the carrier of L:];
coherence
 for b1 being Relation of L st b1 is satisfying_SI holds
b1 is satisfying_INT by Th47;
end;


theorem Th48: :: WAYBEL_4:48
for L being complete LATTICE
for x, y being Element of L
for AR being approximating Relation of L st not x <= y holds
ex u being Element of L st
( [u,x] in AR & not u <= y )
proof
let L be complete LATTICE; ::_thesis: for x, y being Element of L
for AR being approximating Relation of L st not x <= y holds
ex u being Element of L st
( [u,x] in AR & not u <= y )
let x, y be Element of L; ::_thesis: for AR being approximating Relation of L st not x <= y holds
ex u being Element of L st
( [u,x] in AR & not u <= y )
let AR be approximating Relation of L; ::_thesis: ( not x <= y implies ex u being Element of L st
( [u,x] in AR & not u <= y ) )
assume A1: not x <= y ; ::_thesis: ex u being Element of L st
( [u,x] in AR & not u <= y )
A2: x = sup (AR -below x) by Def17;
 ex_sup_of AR -below x,L by YELLOW_0:17;
then  ( y is_>=_than AR -below x implies y >= x ) by A2, YELLOW_0:def_9;
then consider u being Element of L such that
A3: u in AR -below x and
A4: not u <= y by A1, LATTICE3:def_9;
take  u ; ::_thesis: ( [u,x] in AR & not u <= y )
thus  ( [u,x] in AR & not u <= y ) by A3, A4, Th13; ::_thesis: verum
end;

theorem Th49: :: WAYBEL_4:49
for L being complete LATTICE
for x, z being Element of L
for R being auxiliary(i) auxiliary(iii) approximating Relation of L st [x,z] in R & x <> z holds
ex y being Element of L st
( x <= y & [y,z] in R & x <> y )
proof
let L be complete LATTICE; ::_thesis: for x, z being Element of L
for R being auxiliary(i) auxiliary(iii) approximating Relation of L st [x,z] in R & x <> z holds
ex y being Element of L st
( x <= y & [y,z] in R & x <> y )
let x, z be Element of L; ::_thesis: for R being auxiliary(i) auxiliary(iii) approximating Relation of L st [x,z] in R & x <> z holds
ex y being Element of L st
( x <= y & [y,z] in R & x <> y )
let R be auxiliary(i) auxiliary(iii) approximating Relation of L; ::_thesis: ( [x,z] in R & x <> z implies ex y being Element of L st
( x <= y & [y,z] in R & x <> y ) )
assume that
A1: [x,z] in R and
A2: x <> z ; ::_thesis: ex y being Element of L st
( x <= y & [y,z] in R & x <> y )
 x <= z by A1, Def3;
then  x < z by A2, ORDERS_2:def_6;
then  not z < x by ORDERS_2:4;
then  not z <= x by A2, ORDERS_2:def_6;
then consider u being Element of L such that
A3: [u,z] in R and
A4: not u <= x by Th48;
take y = x "\/" u; ::_thesis: ( x <= y & [y,z] in R & x <> y )
thus  x <= y by YELLOW_0:22; ::_thesis: ( [y,z] in R & x <> y )
thus  [y,z] in R by A1, A3, Def5; ::_thesis: x <> y
thus  x <> y by A4, YELLOW_0:24; ::_thesis: verum
end;

theorem Th50: :: WAYBEL_4:50
for L being complete LATTICE
for x, z being Element of L
for R being auxiliary approximating Relation of L st x << z & x <> z holds
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
proof
let L be complete LATTICE; ::_thesis: for x, z being Element of L
for R being auxiliary approximating Relation of L st x << z & x <> z holds
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
let x, z be Element of L; ::_thesis: for R being auxiliary approximating Relation of L st x << z & x <> z holds
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
let R be auxiliary approximating Relation of L; ::_thesis: ( x << z & x <> z implies ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y ) )
assume that
A1: x << z and
A2: x <> z ; ::_thesis: ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
set I =  {  u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R )  }  ;
A3: [(Bottom L),(Bottom L)] in R by Def6;
 [(Bottom L),z] in R by Def6;
then A4: Bottom L in  {  u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R )  }  by A3;
  {  u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R )  }  c= the carrier of L
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in  {  u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R )  }  or v in the carrier of L )
assume  v in  {  u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R )  }  ; ::_thesis: v in the carrier of L
then  ex u1 being Element of L st
( v = u1 & ex y being Element of L st
( [u1,y] in R & [y,z] in R ) ) ;
hence  v in the carrier of L ; ::_thesis: verum
end;
then reconsider I =  {  u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R )  }  as non empty Subset of L by A4;
A5: I is lower
proof
let x1, y1 be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( not x1 in I or not y1 <= x1 or y1 in I )
assume that
A6: x1 in I and
A7: y1 <= x1 ; ::_thesis: y1 in I
consider v1 being Element of L such that
A8: v1 = x1 and
A9: ex s1 being Element of L st
( [v1,s1] in R & [s1,z] in R ) by A6;
consider s1 being Element of L such that
A10: [v1,s1] in R and
A11: [s1,z] in R by A9;
 s1 <= s1 ;
then  [y1,s1] in R by A7, A8, A10, Def4;
hence  y1 in I by A11; ::_thesis: verum
end;
 I is directed
proof
let u1, u2 be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not u1 in I or not u2 in I or ex b1 being Element of the carrier of L st
( b1 in I & u1 <= b1 & u2 <= b1 ) )
assume that
A12: u1 in I and
A13: u2 in I ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in I & u1 <= b1 & u2 <= b1 )
consider v1 being Element of L such that
A14: v1 = u1 and
A15: ex y1 being Element of L st
( [v1,y1] in R & [y1,z] in R ) by A12;
consider v2 being Element of L such that
A16: v2 = u2 and
A17: ex y2 being Element of L st
( [v2,y2] in R & [y2,z] in R ) by A13;
consider y1 being Element of L such that
A18: [v1,y1] in R and
A19: [y1,z] in R by A15;
consider y2 being Element of L such that
A20: [v2,y2] in R and
A21: [y2,z] in R by A17;
take  u1 "\/" u2 ; ::_thesis: ( u1 "\/" u2 in I & u1 <= u1 "\/" u2 & u2 <= u1 "\/" u2 )
A22: [(u1 "\/" u2),(y1 "\/" y2)] in R by A14, A16, A18, A20, Th1;
 [(y1 "\/" y2),z] in R by A19, A21, Def5;
hence  ( u1 "\/" u2 in I & u1 <= u1 "\/" u2 & u2 <= u1 "\/" u2 ) by A22, YELLOW_0:22; ::_thesis: verum
end;
then reconsider I = I as Ideal of L by A5;
 sup I = z
proof
set z9 = sup I;
assume A23: sup I <> z ; ::_thesis: contradiction
A24: I c= R -below z
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in I or a in R -below z )
assume  a in I ; ::_thesis: a in R -below z
then consider u being Element of L such that
A25: a = u and
A26: ex y2 being Element of L st
( [u,y2] in R & [y2,z] in R ) ;
consider y2 being Element of L such that
A27: [u,y2] in R and
A28: [y2,z] in R by A26;
A29: u <= y2 by A27, Def3;
 z <= z ;
then  [u,z] in R by A28, A29, Def4;
hence  a in R -below z by A25; ::_thesis: verum
end;
A30: ex_sup_of I,L by YELLOW_0:17;
 ex_sup_of R -below z,L by YELLOW_0:17;
then A31: sup I <= sup (R -below z) by A24, A30, YELLOW_0:34;
 z = sup (R -below z) by Def17;
then  sup I < z by A23, A31, ORDERS_2:def_6;
then  not z <= sup I by ORDERS_2:6;
then consider y being Element of L such that
A32: [y,z] in R and
A33: not y <= sup I by Th48;
consider u being Element of L such that
A34: [u,y] in R and
A35: not u <= sup I by A33, Th48;
A36: u in I by A32, A34;
 ( sup I = "\/" (I,L) & ex_sup_of I,L iff ( sup I is_>=_than I & ( for b being Element of L st b is_>=_than I holds
sup I <= b ) ) ) by YELLOW_0:30;
hence  contradiction by A35, A36, LATTICE3:def_9, YELLOW_0:17; ::_thesis: verum
end;
then  x in I by A1, WAYBEL_3:20;
then consider v being Element of L such that
A37: v = x and
A38: ex y9 being Element of L st
( [v,y9] in R & [y9,z] in R ) ;
consider y9 being Element of L such that
A39: [v,y9] in R and
A40: [y9,z] in R by A38;
A41: x <= y9 by A37, A39, Def3;
 z <= z ;
then  [x,z] in R by A40, A41, Def4;
then consider y99 being Element of L such that
A42: x <= y99 and
A43: [y99,z] in R and
A44: x <> y99 by A2, Th49;
A45: x < y99 by A42, A44, ORDERS_2:def_6;
set Y = y9 "\/" y99;
A46: y9 <= y9 "\/" y99 by YELLOW_0:22;
 y99 <= y9 "\/" y99 by YELLOW_0:22;
then A47: x <> y9 "\/" y99 by A45, ORDERS_2:7;
 x <= x ;
then A48: [x,(y9 "\/" y99)] in R by A37, A39, A46, Def4;
 [(y9 "\/" y99),z] in R by A40, A43, Def5;
hence  ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y ) by A47, A48; ::_thesis: verum
end;

theorem Th51: :: WAYBEL_4:51
for L being lower-bounded continuous LATTICE holds L -waybelow is satisfying_SI
proof
let L be lower-bounded continuous LATTICE; ::_thesis: L -waybelow is satisfying_SI
set R = L -waybelow ;
thus  L -waybelow is satisfying_SI ::_thesis: verum
proof
let x, z be Element of L; :: according to WAYBEL_4:def_20 ::_thesis: ( [x,z] in L -waybelow & x <> z implies ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y ) )
assume that
A1: [x,z] in L -waybelow and
A2: x <> z ; ::_thesis: ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y )
 x << z by A1, Def1;
hence  ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y ) by A2, Th50; ::_thesis: verum
end;
end;

registration
let L be lower-bounded continuous LATTICE;
clusterL -waybelow  ->  satisfying_SI ;
coherence
 L -waybelow is satisfying_SI by Th51;
end;

theorem Th52: :: WAYBEL_4:52
for L being lower-bounded continuous LATTICE
for x, y being Element of L st x << y holds
ex x9 being Element of L st
( x << x9 & x9 << y )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for x, y being Element of L st x << y holds
ex x9 being Element of L st
( x << x9 & x9 << y )
let x, y be Element of L; ::_thesis: ( x << y implies ex x9 being Element of L st
( x << x9 & x9 << y ) )
set R = L -waybelow ;
assume  x << y ; ::_thesis: ex x9 being Element of L st
( x << x9 & x9 << y )
then  [x,y] in L -waybelow by Def1;
then consider x9 being Element of L such that
A1: [x,x9] in L -waybelow and
A2: [x9,y] in L -waybelow by Def21;
A3: x << x9 by A1, Def1;
 x9 << y by A2, Def1;
hence  ex x9 being Element of L st
( x << x9 & x9 << y ) by A3; ::_thesis: verum
end;

theorem :: WAYBEL_4:53
for L being lower-bounded continuous LATTICE
for x, y being Element of L holds
( x << y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for x, y being Element of L holds
( x << y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) )
let x, y be Element of L; ::_thesis: ( x << y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) )
hereby  ::_thesis: ( ( for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) ) implies x << y )
assume A1: x << y ; ::_thesis: for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d )
let D be non empty directed Subset of L; ::_thesis: ( y <= sup D implies ex d being Element of L st
( d in D & x << d ) )
assume A2: y <= sup D ; ::_thesis: ex d being Element of L st
( d in D & x << d )
consider x9 being Element of L such that
A3: x << x9 and
A4: x9 << y by A1, Th52;
 ex d being Element of L st
( d in D & x9 <= d ) by A2, A4, WAYBEL_3:def_1;
hence  ex d being Element of L st
( d in D & x << d ) by A3, WAYBEL_3:2; ::_thesis: verum
end;
assume A5: for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) ; ::_thesis: x << y
 for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d )
proof
let D be non empty directed Subset of L; ::_thesis: ( y <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
assume  y <= sup D ; ::_thesis: ex d being Element of L st
( d in D & x <= d )
then  ex d being Element of L st
( d in D & x << d ) by A5;
hence  ex d being Element of L st
( d in D & x <= d ) by WAYBEL_3:1; ::_thesis: verum
end;
hence  x << y by WAYBEL_3:def_1; ::_thesis: verum
end;

begin

definition
let L be RelStr ;
let X be Subset of L;
let R be Relation of the carrier of L;
predX is_directed_wrt R means :Def22: :: WAYBEL_4:def 22
 for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & [x,z] in R & [y,z] in R );
end;

:: deftheorem Def22 defines is_directed_wrt WAYBEL_4:def_22_:_
 for L being RelStr
for X being Subset of L
for R being Relation of the carrier of L holds
( X is_directed_wrt R iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & [x,z] in R & [y,z] in R ) );

theorem :: WAYBEL_4:54
for L being RelStr
for X being Subset of L st X is_directed_wrt the InternalRel of L holds
X is directed
proof
let L be RelStr ; ::_thesis: for X being Subset of L st X is_directed_wrt the InternalRel of L holds
X is directed
let X be Subset of L; ::_thesis: ( X is_directed_wrt the InternalRel of L implies X is directed )
assume A1: X is_directed_wrt the InternalRel of L ; ::_thesis: X is directed
let x, y be Element of L; :: 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 L st
( b1 in X & x <= b1 & y <= b1 ) )
assume that
A2: x in X and
A3: y in X ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in X & x <= b1 & y <= b1 )
consider z being Element of L such that
A4: z in X and
A5: [x,z] in the InternalRel of L and
A6: [y,z] in the InternalRel of L by A1, A2, A3, Def22;
take  z ; ::_thesis: ( z in X & x <= z & y <= z )
thus  z in X by A4; ::_thesis: ( x <= z & y <= z )
thus  ( x <= z & y <= z ) by A5, A6, ORDERS_2:def_5; ::_thesis: verum
end;

definition
let X, x be set ;
let R be Relation;
predx is_maximal_wrt X,R means :Def23: :: WAYBEL_4:def 23
( x in X & ( for y being set holds
( not y in X or not y <> x or not [x,y] in R ) ) );
end;

:: deftheorem Def23 defines is_maximal_wrt WAYBEL_4:def_23_:_
 for X, x being set
for R being Relation holds
( x is_maximal_wrt X,R iff ( x in X & ( for y being set holds
( not y in X or not y <> x or not [x,y] in R ) ) ) );

definition
let L be RelStr ;
let X be set ;
let x be Element of L;
predx is_maximal_in X means :Def24: :: WAYBEL_4:def 24
x is_maximal_wrt X, the InternalRel of L;
end;

:: deftheorem Def24 defines is_maximal_in WAYBEL_4:def_24_:_
 for L being RelStr
for X being set
for x being Element of L holds
( x is_maximal_in X iff x is_maximal_wrt X, the InternalRel of L );

theorem :: WAYBEL_4:55
for L being RelStr
for X being set
for x being Element of L holds
( x is_maximal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x < y ) ) ) )
proof
let L be RelStr ; ::_thesis: for X being set
for x being Element of L holds
( x is_maximal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x < y ) ) ) )
let X be set ; ::_thesis: for x being Element of L holds
( x is_maximal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x < y ) ) ) )
let x be Element of L; ::_thesis: ( x is_maximal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x < y ) ) ) )
hereby  ::_thesis: ( x in X & ( for y being Element of L holds
( not y in X or not x < y ) ) implies x is_maximal_in X )
assume  x is_maximal_in X ; ::_thesis: ( x in X & ( for y being Element of L holds
( not b2 in X or not x < b2 ) ) )
then A1: x is_maximal_wrt X, the InternalRel of L by Def24;
hence  x in X by Def23; ::_thesis: for y being Element of L holds
( not b2 in X or not x < b2 )
let y be Element of L; ::_thesis: ( not b1 in X or not x < b1 )
percases ( not y in X or y = x or not [x,y] in the InternalRel of L ) by A1, Def23;
suppose not y in X ; ::_thesis: ( not b1 in X or not x < b1 )
hence  ( not y in X or not x < y ) ; ::_thesis: verum
end;
suppose y = x ; ::_thesis: ( not b1 in X or not x < b1 )
hence  ( not y in X or not x < y ) ; ::_thesis: verum
end;
suppose not [x,y] in the InternalRel of L ; ::_thesis: ( not b1 in X or not x < b1 )
then  not x <= y by ORDERS_2:def_5;
hence  ( not y in X or not x < y ) by ORDERS_2:def_6; ::_thesis: verum
end;
end;
end;
assume that
A2: x in X and
A3: for y being Element of L holds
( not y in X or not x < y ) ; ::_thesis: x is_maximal_in X
assume  not x is_maximal_in X ; ::_thesis: contradiction
then  not x is_maximal_wrt X, the InternalRel of L by Def24;
then consider y being set  such that
A4: y in X and
A5: y <> x and
A6: [x,y] in the InternalRel of L by A2, Def23;
reconsider y = y as Element of L by A6, ZFMISC_1:87;
 x <= y by A6, ORDERS_2:def_5;
then  x < y by A5, ORDERS_2:def_6;
hence  contradiction by A3, A4; ::_thesis: verum
end;

definition
let X, x be set ;
let R be Relation;
predx is_minimal_wrt X,R means :Def25: :: WAYBEL_4:def 25
( x in X & ( for y being set holds
( not y in X or not y <> x or not [y,x] in R ) ) );
end;

:: deftheorem Def25 defines is_minimal_wrt WAYBEL_4:def_25_:_
 for X, x being set
for R being Relation holds
( x is_minimal_wrt X,R iff ( x in X & ( for y being set holds
( not y in X or not y <> x or not [y,x] in R ) ) ) );

definition
let L be RelStr ;
let X be set ;
let x be Element of L;
predx is_minimal_in X means :Def26: :: WAYBEL_4:def 26
x is_minimal_wrt X, the InternalRel of L;
end;

:: deftheorem Def26 defines is_minimal_in WAYBEL_4:def_26_:_
 for L being RelStr
for X being set
for x being Element of L holds
( x is_minimal_in X iff x is_minimal_wrt X, the InternalRel of L );

theorem :: WAYBEL_4:56
for L being RelStr
for X being set
for x being Element of L holds
( x is_minimal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) ) )
proof
let L be RelStr ; ::_thesis: for X being set
for x being Element of L holds
( x is_minimal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) ) )
let X be set ; ::_thesis: for x being Element of L holds
( x is_minimal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) ) )
let x be Element of L; ::_thesis: ( x is_minimal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) ) )
hereby  ::_thesis: ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) implies x is_minimal_in X )
assume  x is_minimal_in X ; ::_thesis: ( x in X & ( for y being Element of L holds
( not b2 in X or not x > b2 ) ) )
then A1: x is_minimal_wrt X, the InternalRel of L by Def26;
hence  x in X by Def25; ::_thesis: for y being Element of L holds
( not b2 in X or not x > b2 )
let y be Element of L; ::_thesis: ( not b1 in X or not x > b1 )
percases ( not y in X or y = x or not [y,x] in the InternalRel of L ) by A1, Def25;
suppose not y in X ; ::_thesis: ( not b1 in X or not x > b1 )
hence  ( not y in X or not x > y ) ; ::_thesis: verum
end;
suppose y = x ; ::_thesis: ( not b1 in X or not x > b1 )
hence  ( not y in X or not x > y ) ; ::_thesis: verum
end;
suppose not [y,x] in the InternalRel of L ; ::_thesis: ( not b1 in X or not b1 < x )
then  not y <= x by ORDERS_2:def_5;
hence  ( not y in X or not y < x ) by ORDERS_2:def_6; ::_thesis: verum
end;
end;
end;
assume that
A2: x in X and
A3: for y being Element of L holds
( not y in X or not x > y ) ; ::_thesis: x is_minimal_in X
assume  not x is_minimal_in X ; ::_thesis: contradiction
then  not x is_minimal_wrt X, the InternalRel of L by Def26;
then consider y being set  such that
A4: y in X and
A5: y <> x and
A6: [y,x] in the InternalRel of L by A2, Def25;
reconsider y = y as Element of L by A6, ZFMISC_1:87;
 y <= x by A6, ORDERS_2:def_5;
then  y < x by A5, ORDERS_2:def_6;
hence  contradiction by A3, A4; ::_thesis: verum
end;

theorem :: WAYBEL_4:57
for L being complete LATTICE
for AR being Relation of L st AR is satisfying_SI holds
for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR
proof
let L be complete LATTICE; ::_thesis: for AR being Relation of L st AR is satisfying_SI holds
for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR
let AR be Relation of L; ::_thesis: ( AR is satisfying_SI implies for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR )
assume A1: AR is satisfying_SI ; ::_thesis: for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR
let x be Element of L; ::_thesis: ( ex y being Element of L st y is_maximal_wrt AR -below x,AR implies [x,x] in AR )
given y being Element of L such that A2: y is_maximal_wrt AR -below x,AR ; ::_thesis: [x,x] in AR
A3: y in AR -below x by A2, Def23;
assume A4: not [x,x] in AR ; ::_thesis: contradiction
A5: [y,x] in AR by A3, Th13;
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: contradiction
hence  contradiction by A3, A4, Th13; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: contradiction
then consider z being Element of L such that
A6: [y,z] in AR and
A7: [z,x] in AR and
A8: z <> y by A1, A5, Def20;
 z in AR -below x by A7;
hence  contradiction by A2, A6, A8, Def23; ::_thesis: verum
end;
end;
end;

theorem :: WAYBEL_4:58
for L being complete LATTICE
for AR being Relation of L st ( for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR ) holds
AR is satisfying_SI
proof
let L be complete LATTICE; ::_thesis: for AR being Relation of L st ( for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR ) holds
AR is satisfying_SI
let AR be Relation of L; ::_thesis: ( ( for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR ) implies AR is satisfying_SI )
assume A1: for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR ; ::_thesis: AR is satisfying_SI
now__::_thesis:_for_z,_x_being_Element_of_L_st_[z,x]_in_AR_&_z_<>_x_holds_
ex_y_being_Element_of_L_st_
(_[z,y]_in_AR_&_[y,x]_in_AR_&_z_<>_y_)
let z, x be Element of L; ::_thesis: ( [z,x] in AR & z <> x implies ex y being Element of L st
( [y,b3] in AR & [b3,b2] in AR & y <> b3 ) )
assume that
A2: [z,x] in AR and
A3: z <> x ; ::_thesis: ex y being Element of L st
( [y,b3] in AR & [b3,b2] in AR & y <> b3 )
A4: z in AR -below x by A2;
percases ( [x,x] in AR or not [x,x] in AR ) ;
suppose [x,x] in AR ; ::_thesis: ex y being Element of L st
( [y,b3] in AR & [b3,b2] in AR & y <> b3 )
hence  ex y being Element of L st
( [z,y] in AR & [y,x] in AR & z <> y ) by A2, A3; ::_thesis: verum
end;
suppose not [x,x] in AR ; ::_thesis: ex y being Element of L st
( [y,b3] in AR & [b3,b2] in AR & y <> b3 )
then  not z is_maximal_wrt AR -below x,AR by A1;
then consider y being set  such that
A5: y in AR -below x and
A6: y <> z and
A7: [z,y] in AR by A4, Def23;
 [y,x] in AR by A5, Th13;
hence  ex y being Element of L st
( [z,y] in AR & [y,x] in AR & z <> y ) by A5, A6, A7; ::_thesis: verum
end;
end;
end;
hence  AR is satisfying_SI by Def20; ::_thesis: verum
end;

theorem :: WAYBEL_4:59
for L being complete LATTICE
for AR being auxiliary(ii) auxiliary(iii) Relation of L st AR is satisfying_INT holds
for x being Element of L holds AR -below x is_directed_wrt AR
proof
let L be complete LATTICE; ::_thesis: for AR being auxiliary(ii) auxiliary(iii) Relation of L st AR is satisfying_INT holds
for x being Element of L holds AR -below x is_directed_wrt AR
let AR be auxiliary(ii) auxiliary(iii) Relation of L; ::_thesis: ( AR is satisfying_INT implies for x being Element of L holds AR -below x is_directed_wrt AR )
assume A1: AR is satisfying_INT ; ::_thesis: for x being Element of L holds AR -below x is_directed_wrt AR
let x be Element of L; ::_thesis: AR -below x is_directed_wrt AR
let y be Element of L; :: according to WAYBEL_4:def_22 ::_thesis: for y being Element of L st y in AR -below x & y in AR -below x holds
ex z being Element of L st
( z in AR -below x & [y,z] in AR & [y,z] in AR )
let z be Element of L; ::_thesis: ( y in AR -below x & z in AR -below x implies ex z being Element of L st
( z in AR -below x & [y,z] in AR & [z,z] in AR ) )
assume that
A2: y in AR -below x and
A3: z in AR -below x ; ::_thesis: ex z being Element of L st
( z in AR -below x & [y,z] in AR & [z,z] in AR )
A4: [y,x] in AR by A2, Th13;
A5: [z,x] in AR by A3, Th13;
consider y9 being Element of L such that
A6: [y,y9] in AR and
A7: [y9,x] in AR by A1, A4, Def21;
consider z9 being Element of L such that
A8: [z,z9] in AR and
A9: [z9,x] in AR by A1, A5, Def21;
take u = y9 "\/" z9; ::_thesis: ( u in AR -below x & [y,u] in AR & [z,u] in AR )
 [u,x] in AR by A7, A9, Def5;
hence  u in AR -below x ; ::_thesis: ( [y,u] in AR & [z,u] in AR )
A10: y <= y ;
 y9 <= u by YELLOW_0:22;
hence  [y,u] in AR by A6, A10, Def4; ::_thesis: [z,u] in AR
A11: z <= z ;
 z9 <= u by YELLOW_0:22;
hence  [z,u] in AR by A8, A11, Def4; ::_thesis: verum
end;

theorem :: WAYBEL_4:60
for L being complete LATTICE
for AR being Relation of L st ( for x being Element of L holds AR -below x is_directed_wrt AR ) holds
AR is satisfying_INT
proof
let L be complete LATTICE; ::_thesis: for AR being Relation of L st ( for x being Element of L holds AR -below x is_directed_wrt AR ) holds
AR is satisfying_INT
let AR be Relation of L; ::_thesis: ( ( for x being Element of L holds AR -below x is_directed_wrt AR ) implies AR is satisfying_INT )
assume A1: for x being Element of L holds AR -below x is_directed_wrt AR ; ::_thesis: AR is satisfying_INT
let X, Z be Element of L; :: according to WAYBEL_4:def_21 ::_thesis: ( [X,Z] in AR implies ex y being Element of L st
( [X,y] in AR & [y,Z] in AR ) )
assume  [X,Z] in AR ; ::_thesis: ex y being Element of L st
( [X,y] in AR & [y,Z] in AR )
then A2: X in AR -below Z ;
 AR -below Z is_directed_wrt AR by A1;
then consider u being Element of L such that
A3: u in AR -below Z and
A4: [X,u] in AR and
 [X,u] in AR by A2, Def22;
take  u ; ::_thesis: ( [X,u] in AR & [u,Z] in AR )
thus  [X,u] in AR by A4; ::_thesis: [u,Z] in AR
thus  [u,Z] in AR by A3, Th13; ::_thesis: verum
end;

theorem Th61: :: WAYBEL_4:61
for L being complete LATTICE
for R being auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of L st R is satisfying_INT holds
R is satisfying_SI
proof
let L be complete LATTICE; ::_thesis: for R being auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of L st R is satisfying_INT holds
R is satisfying_SI
let R be auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of L; ::_thesis: ( R is satisfying_INT implies R is satisfying_SI )
assume A1: R is satisfying_INT ; ::_thesis: R is satisfying_SI
let x be Element of L; :: according to WAYBEL_4:def_20 ::_thesis: for z being Element of L st [x,z] in R & x <> z holds
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
let z be Element of L; ::_thesis: ( [x,z] in R & x <> z implies ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y ) )
assume that
A2: [x,z] in R and
A3: x <> z ; ::_thesis: ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
consider y being Element of L such that
A4: [x,y] in R and
A5: [y,z] in R by A1, A2, Def21;
consider y9 being Element of L such that
A6: x <= y9 and
A7: [y9,z] in R and
A8: x <> y9 by A2, A3, Th49;
A9: x < y9 by A6, A8, ORDERS_2:def_6;
take Y = y "\/" y9; ::_thesis: ( [x,Y] in R & [Y,z] in R & x <> Y )
A10: x <= y by A4, Def3;
A11: x <= x ;
A12: y <= Y by YELLOW_0:22;
percases ( y9 <= y or not y9 <= y ) ;
suppose y9 <= y ; ::_thesis: ( [x,Y] in R & [Y,z] in R & x <> Y )
then  x < y by A9, ORDERS_2:7;
hence  ( [x,Y] in R & [Y,z] in R & x <> Y ) by A4, A5, A7, A11, A12, Def4, Def5, ORDERS_2:7; ::_thesis: verum
end;
suppose not y9 <= y ; ::_thesis: ( [x,Y] in R & [Y,z] in R & x <> Y )
then  y <> Y by YELLOW_0:24;
then  y < Y by A12, ORDERS_2:def_6;
hence  ( [x,Y] in R & [Y,z] in R & x <> Y ) by A4, A5, A7, A10, A11, A12, Def4, Def5, ORDERS_2:7; ::_thesis: verum
end;
end;
end;

registration
let L be complete LATTICE;
cluster auxiliary approximating satisfying_INT  ->  auxiliary approximating satisfying_SI for Element of bool [: the carrier of L, the carrier of L:];
coherence
 for b1 being auxiliary approximating Relation of L st b1 is satisfying_INT holds
b1 is satisfying_SI by Th61;
end;