:: by Adam Grabowski

::

:: Received October 21, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

definition

let L be non empty reflexive RelStr ;

ex b_{1} being Relation of L st

for x, y being Element of L holds

( [x,y] in b_{1} iff x << y )

for b_{1}, b_{2} being Relation of L st ( for x, y being Element of L holds

( [x,y] in b_{1} iff x << y ) ) & ( for x, y being Element of L holds

( [x,y] in b_{2} iff x << y ) ) holds

b_{1} = b_{2}

end;
func L -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 for x, y being Element of L holds

( [x,y] in it iff x << y );

ex b

for x, y being Element of L holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def1 defines -waybelow WAYBEL_4:def 1 :

for L being non empty reflexive RelStr

for b_{2} being Relation of L holds

( b_{2} = L -waybelow iff for x, y being Element of L holds

( [x,y] in b_{2} iff x << y ) );

for L being non empty reflexive RelStr

for b

( b

( [x,y] in b

:: deftheorem defines IntRel WAYBEL_4:def 2 :

for L being RelStr holds IntRel L = the InternalRel of L;

for L being RelStr holds IntRel L = the InternalRel of L;

definition

let L be RelStr ;

let R be Relation of L;

end;
let R be Relation of L;

attr R is auxiliary(i) means :Def3: :: WAYBEL_4:def 3

for x, y being Element of L st [x,y] in R holds

x <= y;

for x, y being Element of L st [x,y] in R holds

x <= y;

:: 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 );

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 );

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;

end;
let R be Relation of L;

attr R 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;

for x, y, z being Element of L st [x,z] in R & [y,z] in R holds

[(x "\/" y),z] in R;

attr R is auxiliary(iv) means :Def6: :: WAYBEL_4:def 6

for x being Element of L holds [(Bottom L),x] in R;

for x being Element of L holds [(Bottom L),x] in R;

:: 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 );

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 );

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 1.9 p.43

definition

let L be non empty RelStr ;

let R be Relation of L;

end;
let R be Relation of L;

attr R is auxiliary means :Def7: :: WAYBEL_4:def 7

( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) );

( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) );

:: 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) ) );

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 ;

for b_{1} being Relation of L st b_{1} is auxiliary holds

( b_{1} is auxiliary(i) & b_{1} is auxiliary(ii) & b_{1} is auxiliary(iii) & b_{1} is auxiliary(iv) )
by Def7;

for b_{1} being Relation of L st b_{1} is auxiliary(i) & b_{1} is auxiliary(ii) & b_{1} is auxiliary(iii) & b_{1} is auxiliary(iv) holds

b_{1} is auxiliary
by Def7;

end;
cluster auxiliary -> auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:];

coherence for b

( b

cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) -> auxiliary for Element of bool [: the carrier of L, the carrier of L:];

coherence for b

b

registration

let L be transitive antisymmetric lower-bounded with_suprema RelStr ;

existence

ex b_{1} being Relation of L st b_{1} is auxiliary

end;
existence

ex b

proof 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

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 end;

Lm1: for L being lower-bounded sup-Semilattice

for AR being auxiliary(i) auxiliary(ii) Relation of L holds AR is transitive

proof end;

registration

let L be lower-bounded sup-Semilattice;

for b_{1} being Relation of L st b_{1} is auxiliary(i) & b_{1} is auxiliary(ii) holds

b_{1} is transitive
by Lm1;

end;
cluster auxiliary(i) auxiliary(ii) -> transitive for Element of bool [: the carrier of L, the carrier of L:];

coherence for b

b

registration
end;

registration
end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;

coherence

IntRel L is auxiliary(iv)

end;
coherence

IntRel L is auxiliary(iv)

proof end;

definition

let L be lower-bounded sup-Semilattice;

ex b_{1} being set st

for a being set holds

( a in b_{1} iff a is auxiliary Relation of L )

for b_{1}, b_{2} being set st ( for a being set holds

( a in b_{1} iff a is auxiliary Relation of L ) ) & ( for a being set holds

( a in b_{2} iff a is auxiliary Relation of L ) ) holds

b_{1} = b_{2}

end;
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 for a being set holds

( a in it iff a is auxiliary Relation of L );

ex b

for a being set holds

( a in b

proof end;

uniqueness for b

( a in b

( a in b

b

proof end;

:: deftheorem Def8 defines Aux WAYBEL_4:def 8 :

for L being lower-bounded sup-Semilattice

for b_{2} being set holds

( b_{2} = Aux L iff for a being set holds

( a in b_{2} iff a is auxiliary Relation of L ) );

for L being lower-bounded sup-Semilattice

for b

( b

( a in b

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 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

for AR being auxiliary(i) Relation of L holds AR c= IntRel L

proof end;

registration
end;

definition

let L be non empty RelStr ;

ex b_{1} being Relation of L st

for x, y being Element of L holds

( [x,y] in b_{1} iff x = Bottom L )

for b_{1}, b_{2} being Relation of L st ( for x, y being Element of L holds

( [x,y] in b_{1} iff x = Bottom L ) ) & ( for x, y being Element of L holds

( [x,y] in b_{2} iff x = Bottom L ) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of L holds

( [x,y] in it iff x = Bottom L );

ex b

for x, y being Element of L holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def9 defines AuxBottom WAYBEL_4:def 9 :

for L being non empty RelStr

for b_{2} being Relation of L holds

( b_{2} = AuxBottom L iff for x, y being Element of L holds

( [x,y] in b_{2} iff x = Bottom L ) );

for L being non empty RelStr

for b

( b

( [x,y] in b

registration
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

for AR being auxiliary(iv) Relation of L holds AuxBottom L c= AR

proof end;

registration
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

for a, b being auxiliary(i) Relation of L holds a /\ b is auxiliary(i) Relation of L

proof 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

for a, b being auxiliary(ii) Relation of L holds a /\ b is auxiliary(ii) Relation of L

proof 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

for a, b being auxiliary(iii) Relation of L holds a /\ b is auxiliary(iii) Relation of L

proof 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

for a, b being auxiliary(iv) Relation of L holds a /\ b is auxiliary(iv) Relation of L

proof 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

for a, b being auxiliary Relation of L holds a /\ b is auxiliary Relation of L

proof 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

for X being non empty Subset of (InclPoset (Aux L)) holds meet X is auxiliary Relation of L

proof end;

registration
end;

registration
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

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

coherence

{ y where y is Element of L : [x,y] in AR } is Subset of L;

by A2;

end;
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 end;

func AR -below x -> Subset of L equals :: WAYBEL_4:def 10

{ y where y is Element of L : [y,x] in AR } ;

correctness { y where y is Element of L : [y,x] in AR } ;

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 end;

func AR -above x -> Subset of L equals :: WAYBEL_4:def 11

{ y where y is Element of L : [x,y] in AR } ;

correctness { y where y is Element of L : [x,y] in AR } ;

coherence

{ y where y is Element of L : [x,y] in AR } is Subset of L;

by A2;

:: 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 } ;

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 } ;

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

for x being Element of L

for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x

proof end;

registration

let L be lower-bounded sup-Semilattice;

let x be Element of L;

let AR be auxiliary(iv) Relation of L;

coherence

not AR -below x is empty

end;
let x be Element of L;

let AR be auxiliary(iv) Relation of L;

coherence

not AR -below x is empty

proof end;

registration

let L be lower-bounded sup-Semilattice;

let x be Element of L;

let AR be auxiliary(ii) Relation of L;

coherence

AR -below x is lower

end;
let x be Element of L;

let AR be auxiliary(ii) Relation of L;

coherence

AR -below x is lower

proof end;

registration

let L be lower-bounded sup-Semilattice;

let x be Element of L;

let AR be auxiliary(iii) Relation of L;

coherence

AR -below x is directed

end;
let x be Element of L;

let AR be auxiliary(iii) Relation of L;

coherence

AR -below x is directed

proof end;

definition

let L be lower-bounded sup-Semilattice;

let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;

ex b_{1} being Function of L,(InclPoset (Ids L)) st

for x being Element of L holds b_{1} . x = AR -below x

for b_{1}, b_{2} being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b_{1} . x = AR -below x ) & ( for x being Element of L holds b_{2} . x = AR -below x ) holds

b_{1} = b_{2}

end;
let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;

func AR -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 for x being Element of L holds it . x = AR -below x;

ex b

for x being Element of L holds b

proof end;

uniqueness for b

b

proof 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 b_{3} being Function of L,(InclPoset (Ids L)) holds

( b_{3} = AR -below iff for x being Element of L holds b_{3} . x = AR -below x );

for L being lower-bounded sup-Semilattice

for AR being auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L

for b

( b

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 )

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 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 )

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 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 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

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 end;

definition

let L be non empty Poset;

ex b_{1} being strict RelStr st

for a being set holds

( ( a in the carrier of b_{1} 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 b_{1} ) & ( for c, d being set holds

( [c,d] in the InternalRel of b_{1} iff ex f, g being Function of L,(InclPoset (Ids L)) st

( c = f & d = g & c in the carrier of b_{1} & d in the carrier of b_{1} & f <= g ) ) ) )

for b_{1}, b_{2} being strict RelStr st ( for a being set holds

( ( a in the carrier of b_{1} 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 b_{1} ) & ( for c, d being set holds

( [c,d] in the InternalRel of b_{1} iff ex f, g being Function of L,(InclPoset (Ids L)) st

( c = f & d = g & c in the carrier of b_{1} & d in the carrier of b_{1} & f <= g ) ) ) ) ) & ( for a being set holds

( ( a in the carrier of b_{2} 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 b_{2} ) & ( for c, d being set holds

( [c,d] in the InternalRel of b_{2} iff ex f, g being Function of L,(InclPoset (Ids L)) st

( c = f & d = g & c in the carrier of b_{2} & d in the carrier of b_{2} & f <= g ) ) ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) ) ) );

ex b

for a being set holds

( ( a in the carrier of b

( 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 b

( [c,d] in the InternalRel of b

( c = f & d = g & c in the carrier of b

proof end;

uniqueness for b

( ( a in the carrier of b

( 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 b

( [c,d] in the InternalRel of b

( c = f & d = g & c in the carrier of b

( ( a in the carrier of b

( 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 b

( [c,d] in the InternalRel of b

( c = f & d = g & c in the carrier of b

b

proof end;

:: deftheorem Def13 defines MonSet WAYBEL_4:def 13 :

for L being non empty Poset

for b_{2} being strict RelStr holds

( b_{2} = MonSet L iff for a being set holds

( ( a in the carrier of b_{2} 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 b_{2} ) & ( for c, d being set holds

( [c,d] in the InternalRel of b_{2} iff ex f, g being Function of L,(InclPoset (Ids L)) st

( c = f & d = g & c in the carrier of b_{2} & d in the carrier of b_{2} & f <= g ) ) ) ) );

for L being non empty Poset

for b

( b

( ( a in the carrier of b

( 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 b

( [c,d] in the InternalRel of b

( c = f & d = g & c in the carrier of b

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 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

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 end;

registration

let L be lower-bounded sup-Semilattice;

let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;

coherence

AR -below is monotone

end;
let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;

coherence

AR -below is monotone

proof 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)

for AR being auxiliary Relation of L holds AR -below in the carrier of (MonSet L)

proof end;

theorem :: WAYBEL_4:20

for L being lower-bounded sup-Semilattice

for AR being auxiliary Relation of L holds AR -below <= IdsMap L

for AR being auxiliary Relation of L holds AR -below <= IdsMap L

proof end;

Lm4: for L being lower-bounded sup-Semilattice

for I being Ideal of L holds {(Bottom L)} c= I

proof 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 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 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 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)

for AR being auxiliary Relation of L holds [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L)

proof 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 end;

registration
end;

definition

let L be lower-bounded sup-Semilattice;

ex b_{1} being Function of (InclPoset (Aux L)),(MonSet L) st

for AR being auxiliary Relation of L holds b_{1} . AR = AR -below

for b_{1}, b_{2} being Function of (InclPoset (Aux L)),(MonSet L) st ( for AR being auxiliary Relation of L holds b_{1} . AR = AR -below ) & ( for AR being auxiliary Relation of L holds b_{2} . AR = AR -below ) holds

b_{1} = b_{2}

end;
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 for AR being auxiliary Relation of L holds it . AR = AR -below ;

ex b

for AR being auxiliary Relation of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines Rel2Map WAYBEL_4:def 14 :

for L being lower-bounded sup-Semilattice

for b_{2} being Function of (InclPoset (Aux L)),(MonSet L) holds

( b_{2} = Rel2Map L iff for AR being auxiliary Relation of L holds b_{2} . AR = AR -below );

for L being lower-bounded sup-Semilattice

for b

( b

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

for R1, R2 being auxiliary Relation of L st R1 c= R2 holds

R1 -below <= R2 -below

proof 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

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 end;

Lm7: for L being lower-bounded sup-Semilattice holds Rel2Map L is monotone

proof end;

definition

let L be lower-bounded sup-Semilattice;

ex b_{1} 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 = b_{1} . 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 b_{1}, b_{2} 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 = b_{1} . 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 = b_{2} . 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

b_{1} = b_{2}

end;
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 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 ) ) ) );

ex b

for s being set st s in the carrier of (MonSet L) holds

ex AR being auxiliary Relation of L st

( AR = b

( [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 end;

uniqueness for b

ex AR being auxiliary Relation of L st

( AR = b

( [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 = b

( [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

b

proof end;

:: deftheorem Def15 defines Map2Rel WAYBEL_4:def 15 :

for L being lower-bounded sup-Semilattice

for b_{2} being Function of (MonSet L),(InclPoset (Aux L)) holds

( b_{2} = 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 = b_{2} . 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 L being lower-bounded sup-Semilattice

for b

( b

ex AR being auxiliary Relation of L st

( AR = b

( [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 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 end;

registration
end;

:: Proposition 1.10 (i) p.43

:: Proposition 1.10 (ii) p.43

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

for x being Element of L holds meet { I where I is Ideal of L : x <= sup I } = waybelow x

proof end;

definition

let L be Semilattice;

let I be Ideal of L;

ex b_{1} being Function of L,(InclPoset (Ids L)) st

for x being Element of L holds

( ( x <= sup I implies b_{1} . x = (downarrow x) /\ I ) & ( not x <= sup I implies b_{1} . x = downarrow x ) )

for b_{1}, b_{2} being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds

( ( x <= sup I implies b_{1} . x = (downarrow x) /\ I ) & ( not x <= sup I implies b_{1} . x = downarrow x ) ) ) & ( for x being Element of L holds

( ( x <= sup I implies b_{2} . x = (downarrow x) /\ I ) & ( not x <= sup I implies b_{2} . x = downarrow x ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for x being Element of L holds

( ( x <= sup I implies b

proof end;

uniqueness for b

( ( x <= sup I implies b

( ( x <= sup I implies b

b

proof end;

:: deftheorem Def16 defines DownMap WAYBEL_4:def 16 :

for L being Semilattice

for I being Ideal of L

for b_{3} being Function of L,(InclPoset (Ids L)) holds

( b_{3} = DownMap I iff for x being Element of L holds

( ( x <= sup I implies b_{3} . x = (downarrow x) /\ I ) & ( not x <= sup I implies b_{3} . x = downarrow x ) ) );

for L being Semilattice

for I being Ideal of L

for b

( b

( ( x <= sup I implies b

Lm9: for L being Semilattice

for I being Ideal of L holds DownMap I is monotone

proof 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 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

for x being Element of L

for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D

proof end;

begin

:: Definition 1.11 p.44

definition

let L be non empty RelStr ;

let AR be Relation of L;

end;
let AR be Relation of L;

attr AR is approximating means :Def17: :: WAYBEL_4:def 17

for x being Element of L holds x = sup (AR -below x);

for x being Element of L holds x = sup (AR -below x);

:: 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) );

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));

end;
let mp be Function of L,(InclPoset (Ids L));

attr mp 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 );

for x being Element of L ex ii being Subset of L st

( ii = mp . x & x = sup ii );

:: 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 ) );

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 ) );

:: Lemma 1.12 (i) p.44

theorem Th37: :: WAYBEL_4:37

for L being lower-bounded meet-continuous Semilattice

for I being Ideal of L holds DownMap I is approximating

for I being Ideal of L holds DownMap I is approximating

proof 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 end;

:: Lemma 1.12 (ii) p.44

registration

for b_{1} being lower-bounded LATTICE st b_{1} is continuous holds

b_{1} is meet-continuous
by Th38;

end;

cluster reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous -> lower-bounded meet-continuous for RelStr ;

coherence for b

b

:: Lemma 1.12 (iii) p.44

theorem :: WAYBEL_4:39

for L being lower-bounded continuous LATTICE

for I being Ideal of L holds DownMap I is approximating by Th37;

for I being Ideal of L holds DownMap I is approximating by Th37;

registration

let L be non empty reflexive antisymmetric RelStr ;

coherence

L -waybelow is auxiliary(i)

end;
coherence

L -waybelow is auxiliary(i)

proof end;

registration
end;

registration
end;

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;

coherence

L -waybelow is auxiliary(iv)

end;
coherence

L -waybelow is auxiliary(iv)

proof end;

Lm12: for L being lower-bounded continuous LATTICE holds L -waybelow is approximating

proof end;

registration
end;

registration

let L be complete LATTICE;

ex b_{1} being Relation of L st

( b_{1} is approximating & b_{1} is auxiliary )

end;
cluster Relation-like auxiliary approximating for Element of bool [: the carrier of L, the carrier of L:];

existence ex b

( b

proof end;

definition

let L be complete LATTICE;

defpred S_{1}[ set ] means $1 is auxiliary approximating Relation of L;

ex b_{1} being set st

for a being set holds

( a in b_{1} iff a is auxiliary approximating Relation of L )

for b_{1}, b_{2} being set st ( for a being set holds

( a in b_{1} iff a is auxiliary approximating Relation of L ) ) & ( for a being set holds

( a in b_{2} iff a is auxiliary approximating Relation of L ) ) holds

b_{1} = b_{2}

end;
defpred S

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 for a being set holds

( a in it iff a is auxiliary approximating Relation of L );

ex b

for a being set holds

( a in b

proof end;

uniqueness for b

( a in b

( a in b

b

proof end;

:: deftheorem Def19 defines App WAYBEL_4:def 19 :

for L being complete LATTICE

for b_{2} being set holds

( b_{2} = App L iff for a being set holds

( a in b_{2} iff a is auxiliary approximating Relation of L ) );

for L being complete LATTICE

for b

( b

( a in b

registration
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

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 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

for x being Element of L holds meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x

proof end;

:: Proposition 1.13 p.45

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

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 end;

:: Proposition 1.14 p.45 ( 1 <=> 2 )

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 ) )

( L is continuous iff for R being auxiliary approximating Relation of L holds

( L -waybelow c= R & L -waybelow is approximating ) )

proof end;

:: Proposition 1.14 p.45 ( 1 <=> 3 )

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 ) )

( 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 end;

:: Definition 1.15 (SI) p.46

:: 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 ) );

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 1.15 (INT) p.46

:: 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 ) );

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 ) );

registration

let L be non empty RelStr ;

for b_{1} being Relation of L st b_{1} is satisfying_SI holds

b_{1} is satisfying_INT
by Th47;

end;
cluster satisfying_SI -> satisfying_INT for Element of bool [: the carrier of L, the carrier of L:];

coherence for b

b

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 )

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 end;

:: Lemma 1.16 p.46

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 )

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 end;

:: Lemma 1.17 p.46

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 )

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 end;

:: Theorem 1.18 p.47

registration
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 )

for x, y being Element of L st x << y holds

ex x9 being Element of L st

( x << x9 & x9 << y )

proof end;

:: Corollary 1.19 p.47

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 ) )

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 end;

begin

:: 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 ) );

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

for X being Subset of L st X is_directed_wrt the InternalRel of L holds

X is directed

proof end;

definition

let X, x be set ;

let R be Relation;

end;
let R be Relation;

pred x 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 ) ) );

( x in X & ( for y being set holds

( not y in X or not y <> x or not [x,y] in R ) ) );

:: 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 ) ) ) );

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 ) ) ) );

:: 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 );

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 ) ) ) )

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 end;

definition

let X, x be set ;

let R be Relation;

end;
let R be Relation;

pred x 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 ) ) );

( x in X & ( for y being set holds

( not y in X or not y <> x or not [y,x] in R ) ) );

:: 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 ) ) ) );

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 ) ) ) );

:: 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 );

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 ) ) ) )

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 end;

:: Exercise 1.23 (i) ( 1 => 2 )

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

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 end;

:: Exercise 1.23 (i) ( 2 => 1 )

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

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 end;

:: Exercise 1.23 (ii) ( 3 => 4 )

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

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 end;

:: Exercise 1.23 (ii) ( 4 => 3 )

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

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 end;

:: Exercise 1.23 (iii) p.51

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

for R being auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of L st R is satisfying_INT holds

R is satisfying_SI

proof end;

registration

let L be complete LATTICE;

for b_{1} being auxiliary approximating Relation of L st b_{1} is satisfying_INT holds

b_{1} is satisfying_SI
by Th61;

end;
cluster auxiliary approximating satisfying_INT -> auxiliary approximating satisfying_SI for Element of bool [: the carrier of L, the carrier of L:];

coherence for b

b