:: by Artur Korni{\l}owicz

::

:: Received February 6, 2003

:: Copyright (c) 2003-2017 Association of Mizar Users

Lm1: for x, y, X being set holds

( not y in {x} \/ X or y = x or y in X )

proof end;

registration

let L be RelStr ;

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

end;
cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) for Element of bool [: the carrier of L, the carrier of L:];

existence ex b

proof end;

registration

let L be transitive RelStr ;

ex b_{1} being Relation of L st

( b_{1} is auxiliary(i) & b_{1} is auxiliary(ii) )

end;
cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) for Element of bool [: the carrier of L, the carrier of L:];

existence ex b

( b

proof end;

registration

let L be antisymmetric with_suprema RelStr ;

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

end;
cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iii) for Element of bool [: the carrier of L, the carrier of L:];

existence ex b

proof end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;

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

end;
cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:];

existence ex b

proof end;

:: Definition 2.1, p. 203

definition

let L be non empty RelStr ;

let R be Relation of L;

end;
let R be Relation of L;

attr R is extra-order means :: WAYBEL35:def 1

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

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

:: deftheorem defines extra-order WAYBEL35:def 1 :

for L being non empty RelStr

for R being Relation of L holds

( R is extra-order iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iv) ) );

for L being non empty RelStr

for R being Relation of L holds

( R is extra-order iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iv) ) );

registration

let L be non empty RelStr ;

for b_{1} being Relation of L st b_{1} is extra-order holds

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

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

b_{1} is extra-order
;

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

coherence for b

( b

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

coherence for b

b

registration

let L be non empty RelStr ;

for b_{1} being Relation of L st b_{1} is extra-order & b_{1} is auxiliary(iii) holds

b_{1} is auxiliary
;

coherence

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

b_{1} is extra-order
;

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

coherence for b

b

coherence

for b

b

registration

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

ex b_{1} being Relation of L st b_{1} is extra-order

end;
cluster Relation-like the carrier of L -defined the carrier of L -valued extra-order for Element of bool [: the carrier of L, the carrier of L:];

existence ex b

proof end;

definition

let L be lower-bounded with_suprema Poset;

let R be auxiliary(ii) Relation of L;

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

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

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

b_{1} = b_{2}

end;
let R be auxiliary(ii) Relation of L;

func R -LowerMap -> Function of L,(InclPoset (LOWER L)) means :Def2: :: WAYBEL35:def 2

for x being Element of L holds it . x = R -below x;

existence for x being Element of L holds it . x = R -below x;

ex b

for x being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines -LowerMap WAYBEL35:def 2 :

for L being lower-bounded with_suprema Poset

for R being auxiliary(ii) Relation of L

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

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

for L being lower-bounded with_suprema Poset

for R being auxiliary(ii) Relation of L

for b

( b

registration

let L be lower-bounded with_suprema Poset;

let R be auxiliary(ii) Relation of L;

coherence

R -LowerMap is monotone

end;
let R be auxiliary(ii) Relation of L;

coherence

R -LowerMap is monotone

proof end;

definition

let L be 1-sorted ;

let R be Relation of the carrier of L;

ex b_{1} being Subset of L st

for x, y being set st x in b_{1} & y in b_{1} & not [x,y] in R & not x = y holds

[y,x] in R

end;
let R be Relation of the carrier of L;

mode strict_chain of R -> Subset of L means :Def3: :: WAYBEL35:def 3

for x, y being set st x in it & y in it & not [x,y] in R & not x = y holds

[y,x] in R;

existence for x, y being set st x in it & y in it & not [x,y] in R & not x = y holds

[y,x] in R;

ex b

for x, y being set st x in b

[y,x] in R

proof end;

:: deftheorem Def3 defines strict_chain WAYBEL35:def 3 :

for L being 1-sorted

for R being Relation of the carrier of L

for b_{3} being Subset of L holds

( b_{3} is strict_chain of R iff for x, y being set st x in b_{3} & y in b_{3} & not [x,y] in R & not x = y holds

[y,x] in R );

for L being 1-sorted

for R being Relation of the carrier of L

for b

( b

[y,x] in R );

theorem Th1: :: WAYBEL35:1

for L being 1-sorted

for C being trivial Subset of L

for R being Relation of the carrier of L holds C is strict_chain of R

for C being trivial Subset of L

for R being Relation of the carrier of L holds C is strict_chain of R

proof end;

registration

let L be non empty 1-sorted ;

let R be Relation of the carrier of L;

existence

ex b_{1} being strict_chain of R st b_{1} is 1 -element

end;
let R be Relation of the carrier of L;

existence

ex b

proof end;

theorem Th2: :: WAYBEL35:2

for L being antisymmetric RelStr

for R being auxiliary(i) Relation of L

for C being strict_chain of R

for x, y being Element of L st x in C & y in C & x < y holds

[x,y] in R

for R being auxiliary(i) Relation of L

for C being strict_chain of R

for x, y being Element of L st x in C & y in C & x < y holds

[x,y] in R

proof end;

theorem :: WAYBEL35:3

for L being antisymmetric RelStr

for R being auxiliary(i) Relation of L

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

x = y

for R being auxiliary(i) Relation of L

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

x = y

proof end;

theorem :: WAYBEL35:4

for L being non empty antisymmetric lower-bounded RelStr

for x being Element of L

for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R

for x being Element of L

for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R

proof end;

theorem Th5: :: WAYBEL35:5

for L being non empty antisymmetric lower-bounded RelStr

for R being auxiliary(iv) Relation of L

for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R

for R being auxiliary(iv) Relation of L

for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R

proof end;

definition
end;

:: deftheorem defines maximal WAYBEL35:def 4 :

for L being 1-sorted

for R being Relation of the carrier of L

for C being strict_chain of R holds

( C is maximal iff for D being strict_chain of R st C c= D holds

C = D );

for L being 1-sorted

for R being Relation of the carrier of L

for C being strict_chain of R holds

( C is maximal iff for D being strict_chain of R st C c= D holds

C = D );

definition

let L be 1-sorted ;

let R be Relation of the carrier of L;

let C be set ;

defpred S_{1}[ set ] means ( $1 is strict_chain of R & C c= $1 );

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x is strict_chain of R & C c= x ) )

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

( x in b_{1} iff ( x is strict_chain of R & C c= x ) ) ) & ( for x being set holds

( x in b_{2} iff ( x is strict_chain of R & C c= x ) ) ) holds

b_{1} = b_{2}

end;
let R be Relation of the carrier of L;

let C be set ;

defpred S

func Strict_Chains (R,C) -> set means :Def5: :: WAYBEL35:def 5

for x being set holds

( x in it iff ( x is strict_chain of R & C c= x ) );

existence for x being set holds

( x in it iff ( x is strict_chain of R & C c= x ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def5 defines Strict_Chains WAYBEL35:def 5 :

for L being 1-sorted

for R being Relation of the carrier of L

for C, b_{4} being set holds

( b_{4} = Strict_Chains (R,C) iff for x being set holds

( x in b_{4} iff ( x is strict_chain of R & C c= x ) ) );

for L being 1-sorted

for R being Relation of the carrier of L

for C, b

( b

( x in b

registration

let L be 1-sorted ;

let R be Relation of the carrier of L;

let C be strict_chain of R;

coherence

not Strict_Chains (R,C) is empty by Def5;

end;
let R be Relation of the carrier of L;

let C be strict_chain of R;

coherence

not Strict_Chains (R,C) is empty by Def5;

notation
end;

:: Lemma 2.2, p. 203

theorem :: WAYBEL35:6

for L being 1-sorted

for R being Relation of the carrier of L

for C being strict_chain of R holds

( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st

( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) )

for R being Relation of the carrier of L

for C being strict_chain of R holds

( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st

( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) )

proof end;

:: Lemma 2.3 (ii), p. 203

:: It is a trivial consequence of YELLOW_0:65

:: Maybe to cancel

:: It is a trivial consequence of YELLOW_0:65

:: Maybe to cancel

theorem Th7: :: WAYBEL35:7

for L being non empty transitive RelStr

for C being non empty Subset of L

for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds

( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) )

for C being non empty Subset of L

for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds

( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) )

proof end;

Lm2: for L being non empty Poset

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being non empty strict_chain of R

for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds

ex cs being Element of L st

( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a ) ) )

proof end;

:: Lemma 2.3, p. 203

theorem Th8: :: WAYBEL35:8

for L being non empty Poset

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being non empty strict_chain of R

for X being Subset of C st ex_sup_of X,L & C is maximal holds

ex_sup_of X, subrelstr C

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being non empty strict_chain of R

for X being Subset of C st ex_sup_of X,L & C is maximal holds

ex_sup_of X, subrelstr C

proof end;

:: Lemma 2.3 (i), (iii), p. 203

theorem :: WAYBEL35:9

for L being non empty Poset

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being non empty strict_chain of R

for X being Subset of C st ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal holds

( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) )

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being non empty strict_chain of R

for X being Subset of C st ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal holds

( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) )

proof end;

:: Proposition 2.4, p. 204

theorem :: WAYBEL35:10

for L being non empty complete Poset

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being non empty strict_chain of R st C is maximal holds

subrelstr C is complete

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being non empty strict_chain of R st C is maximal holds

subrelstr C is complete

proof end;

:: Proposition 2.5 (i), p. 204

theorem :: WAYBEL35:11

for L being non empty antisymmetric lower-bounded RelStr

for R being auxiliary(iv) Relation of L

for C being strict_chain of R st C is maximal holds

Bottom L in C

for R being auxiliary(iv) Relation of L

for C being strict_chain of R st C is maximal holds

Bottom L in C

proof end;

:: Proposition 2.5 (ii), p. 204

theorem :: WAYBEL35:12

for L being non empty upper-bounded Poset

for R being auxiliary(ii) Relation of L

for C being strict_chain of R

for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds

( [(Top L),(Top L)] in R & m = Top L )

for R being auxiliary(ii) Relation of L

for C being strict_chain of R

for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds

( [(Top L),(Top L)] in R & m = Top L )

proof end;

:: Definition (SI_C) p. 204

:: deftheorem defines satisfies_SIC_on WAYBEL35:def 6 :

for L being RelStr

for C being set

for R being Relation of the carrier of L holds

( R satisfies_SIC_on C iff for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds

ex y being Element of L st

( y in C & [x,y] in R & [y,z] in R & x <> y ) );

for L being RelStr

for C being set

for R being Relation of the carrier of L holds

( R satisfies_SIC_on C iff for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds

ex y being Element of L st

( y in C & [x,y] in R & [y,z] in R & x <> y ) );

:: deftheorem Def7 defines satisfying_SIC WAYBEL35:def 7 :

for L being RelStr

for R being Relation of the carrier of L

for C being strict_chain of R holds

( C is satisfying_SIC iff R satisfies_SIC_on C );

for L being RelStr

for R being Relation of the carrier of L

for C being strict_chain of R holds

( C is satisfying_SIC iff R satisfies_SIC_on C );

theorem Th13: :: WAYBEL35:13

for L being RelStr

for C being set

for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds

for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds

ex y being Element of L st

( y in C & [x,y] in R & [y,z] in R & x < y )

for C being set

for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds

for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds

ex y being Element of L st

( y in C & [x,y] in R & [y,z] in R & x < y )

proof end;

registration

let L be RelStr ;

let R be Relation of the carrier of L;

coherence

for b_{1} being strict_chain of R st b_{1} is trivial holds

b_{1} is satisfying_SIC

end;
let R be Relation of the carrier of L;

coherence

for b

b

proof end;

registration

let L be non empty RelStr ;

let R be Relation of the carrier of L;

existence

ex b_{1} being strict_chain of R st b_{1} is 1 -element

end;
let R be Relation of the carrier of L;

existence

ex b

proof end;

:: Proposition 2.5 (iii), p. 204

theorem :: WAYBEL35:14

for L being lower-bounded with_suprema Poset

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being strict_chain of R st C is maximal & R is satisfying_SI holds

R satisfies_SIC_on C

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being strict_chain of R st C is maximal & R is satisfying_SI holds

R satisfies_SIC_on C

proof end;

:: deftheorem defines SetBelow WAYBEL35:def 8 :

for R being Relation

for C being set

for y being object holds SetBelow (R,C,y) = (R " {y}) /\ C;

for R being Relation

for C being set

for y being object holds SetBelow (R,C,y) = (R " {y}) /\ C;

theorem Th15: :: WAYBEL35:15

for R being Relation

for C, x, y being set holds

( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) )

for C, x, y being set holds

( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) )

proof end;

definition

let L be 1-sorted ;

let R be Relation of the carrier of L;

let C be set ;

let y be object ;

:: original: SetBelow

redefine func SetBelow (R,C,y) -> Subset of L;

coherence

SetBelow (R,C,y) is Subset of L

end;
let R be Relation of the carrier of L;

let C be set ;

let y be object ;

:: original: SetBelow

redefine func SetBelow (R,C,y) -> Subset of L;

coherence

SetBelow (R,C,y) is Subset of L

proof end;

theorem Th16: :: WAYBEL35:16

for L being RelStr

for R being auxiliary(i) Relation of L

for C being set

for y being Element of L holds SetBelow (R,C,y) is_<=_than y

for R being auxiliary(i) Relation of L

for C being set

for y being Element of L holds SetBelow (R,C,y) is_<=_than y

proof end;

theorem Th17: :: WAYBEL35:17

for L being reflexive transitive RelStr

for R being auxiliary(ii) Relation of L

for C being Subset of L

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

SetBelow (R,C,x) c= SetBelow (R,C,y)

for R being auxiliary(ii) Relation of L

for C being Subset of L

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

SetBelow (R,C,x) c= SetBelow (R,C,y)

proof end;

theorem Th18: :: WAYBEL35:18

for L being RelStr

for R being auxiliary(i) Relation of L

for C being set

for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds

x = sup (SetBelow (R,C,x))

for R being auxiliary(i) Relation of L

for C being set

for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds

x = sup (SetBelow (R,C,x))

proof end;

definition

let L be RelStr ;

let C be Subset of L;

end;
let C be Subset of L;

attr C is sup-closed means :: WAYBEL35:def 9

for X being Subset of C st ex_sup_of X,L holds

"\/" (X,L) = "\/" (X,(subrelstr C));

for X being Subset of C st ex_sup_of X,L holds

"\/" (X,L) = "\/" (X,(subrelstr C));

:: deftheorem defines sup-closed WAYBEL35:def 9 :

for L being RelStr

for C being Subset of L holds

( C is sup-closed iff for X being Subset of C st ex_sup_of X,L holds

"\/" (X,L) = "\/" (X,(subrelstr C)) );

for L being RelStr

for C being Subset of L holds

( C is sup-closed iff for X being Subset of C st ex_sup_of X,L holds

"\/" (X,L) = "\/" (X,(subrelstr C)) );

:: Lemma 2.6, p. 205

theorem Th19: :: WAYBEL35:19

for L being non empty complete Poset

for R being extra-order Relation of L

for C being satisfying_SIC strict_chain of R

for p, q being Element of L st p in C & q in C & p < q holds

ex y being Element of L st

( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )

for R being extra-order Relation of L

for C being satisfying_SIC strict_chain of R

for p, q being Element of L st p in C & q in C & p < q holds

ex y being Element of L st

( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )

proof end;

:: Lemma 2.7, p. 205, 1 => 2

theorem :: WAYBEL35:20

for L being non empty lower-bounded Poset

for R being extra-order Relation of L

for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds

for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c))

for R being extra-order Relation of L

for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds

for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c))

proof end;

:: Lemma 2.7, p. 205, 2 => 1

theorem :: WAYBEL35:21

for L being non empty reflexive antisymmetric RelStr

for R being auxiliary(i) Relation of L

for C being strict_chain of R st ( for c being Element of L st c in C holds

( ex_sup_of SetBelow (R,C,c),L & c = sup (SetBelow (R,C,c)) ) ) holds

R satisfies_SIC_on C

for R being auxiliary(i) Relation of L

for C being strict_chain of R st ( for c being Element of L st c in C holds

( ex_sup_of SetBelow (R,C,c),L & c = sup (SetBelow (R,C,c)) ) ) holds

R satisfies_SIC_on C

proof end;

definition

let L be non empty RelStr ;

let R be Relation of the carrier of L;

let C be set ;

defpred S_{1}[ set ] means $1 = sup (SetBelow (R,C,$1));

ex b_{1} being set st

for y being set holds

( y in b_{1} iff y = sup (SetBelow (R,C,y)) )

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

( y in b_{1} iff y = sup (SetBelow (R,C,y)) ) ) & ( for y being set holds

( y in b_{2} iff y = sup (SetBelow (R,C,y)) ) ) holds

b_{1} = b_{2}

end;
let R be Relation of the carrier of L;

let C be set ;

defpred S

func SupBelow (R,C) -> set means :Def10: :: WAYBEL35:def 10

for y being set holds

( y in it iff y = sup (SetBelow (R,C,y)) );

existence for y being set holds

( y in it iff y = sup (SetBelow (R,C,y)) );

ex b

for y being set holds

( y in b

proof end;

uniqueness for b

( y in b

( y in b

b

proof end;

:: deftheorem Def10 defines SupBelow WAYBEL35:def 10 :

for L being non empty RelStr

for R being Relation of the carrier of L

for C, b_{4} being set holds

( b_{4} = SupBelow (R,C) iff for y being set holds

( y in b_{4} iff y = sup (SetBelow (R,C,y)) ) );

for L being non empty RelStr

for R being Relation of the carrier of L

for C, b

( b

( y in b

definition

let L be non empty RelStr ;

let R be Relation of the carrier of L;

let C be set ;

:: original: SupBelow

redefine func SupBelow (R,C) -> Subset of L;

coherence

SupBelow (R,C) is Subset of L

end;
let R be Relation of the carrier of L;

let C be set ;

:: original: SupBelow

redefine func SupBelow (R,C) -> Subset of L;

coherence

SupBelow (R,C) is Subset of L

proof end;

:: Lemma 2.8, (i) a), p. 205

theorem Th22: :: WAYBEL35:22

for L being non empty reflexive transitive RelStr

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds

SupBelow (R,C) is strict_chain of R

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds

SupBelow (R,C) is strict_chain of R

proof end;

:: Lemma 2.8, (i) b), p. 205

theorem :: WAYBEL35:23

for L being non empty Poset

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being Subset of L st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds

SupBelow (R,C) is sup-closed

for R being auxiliary(i) auxiliary(ii) Relation of L

for C being Subset of L st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds

SupBelow (R,C) is sup-closed

proof end;

theorem Th24: :: WAYBEL35:24

for L being non empty complete Poset

for R being extra-order Relation of L

for C being satisfying_SIC strict_chain of R

for d being Element of L st d in SupBelow (R,C) holds

d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L)

for R being extra-order Relation of L

for C being satisfying_SIC strict_chain of R

for d being Element of L st d in SupBelow (R,C) holds

d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L)

proof end;

:: Lemma 2.8, (ii), p. 205

theorem :: WAYBEL35:25

for L being non empty complete Poset

for R being extra-order Relation of L

for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C)

for R being extra-order Relation of L

for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C)

proof end;

:: Lemma 2.8, (iii), p. 205

theorem :: WAYBEL35:26

for L being non empty complete Poset

for R being extra-order Relation of L

for C being satisfying_SIC strict_chain of R

for a, b being Element of L st a in C & b in C & a < b holds

ex d being Element of L st

( d in SupBelow (R,C) & a < d & [d,b] in R )

for R being extra-order Relation of L

for C being satisfying_SIC strict_chain of R

for a, b being Element of L st a in C & b in C & a < b holds

ex d being Element of L st

( d in SupBelow (R,C) & a < d & [d,b] in R )

proof end;