begin
Lm1:
for x, y, X being set holds
( not y in {x} \/ X or y = x or y in X )
begin
:: deftheorem Def1 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) ) );
:: deftheorem Def2 defines -LowerMap WAYBEL35:def 2 :
for L being lower-bounded with_suprema Poset
for R being auxiliary(ii) Relation of L
for b3 being Function of L,(InclPoset (LOWER L)) holds
( b3 = R -LowerMap iff for x being Element of L holds b3 . x = R -below x );
:: deftheorem Def3 defines strict_chain WAYBEL35:def 3 :
for L being 1-sorted
for R being Relation of the carrier of L
for b3 being Subset of L holds
( b3 is strict_chain of R iff for x, y being set st x in b3 & y in b3 & not [x,y] in R & not x = y holds
[y,x] in R );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
theorem
theorem Th8:
:: deftheorem Def4 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 );
:: deftheorem Def5 defines Strict_Chains WAYBEL35:def 5 :
for L being 1-sorted
for R being Relation of the carrier of L
for C being set
for b4 being set holds
( b4 = Strict_Chains R,C iff for x being set holds
( x in b4 iff ( x is strict_chain of R & C c= x ) ) );
theorem
theorem Th10:
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 ) ) )
theorem Th11:
theorem
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 ) )
theorem
theorem
theorem
:: deftheorem Def6 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 ) );
:: 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 );
theorem Th16:
theorem
:: deftheorem defines SetBelow WAYBEL35:def 8 :
for R being Relation
for C, y being set holds SetBelow R,C,y = (R " {y}) /\ C;
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
:: deftheorem Def9 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) );
theorem Th22:
theorem
theorem
definition
let L be non
empty RelStr ;
let R be
Relation of the
carrier of
L;
let C be
set ;
func SupBelow R,
C -> set means :
Def10:
for
y being
set holds
(
y in it iff
y = sup (SetBelow R,C,y) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff y = sup (SetBelow R,C,y) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff y = sup (SetBelow R,C,y) ) ) & ( for y being set holds
( y in b2 iff y = sup (SetBelow R,C,y) ) ) holds
b1 = b2
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 being set
for b4 being set holds
( b4 = SupBelow R,C iff for y being set holds
( y in b4 iff y = sup (SetBelow R,C,y) ) );
theorem Th25:
theorem
theorem Th27:
theorem
theorem