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 :
:: deftheorem Def2 defines -LowerMap WAYBEL35:def 2 :
:: deftheorem Def3 defines strict_chain WAYBEL35:def 3 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
theorem
theorem Th8:
:: deftheorem Def4 defines maximal WAYBEL35:def 4 :
:: deftheorem Def5 defines Strict_Chains WAYBEL35:def 5 :
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 :
:: deftheorem Def7 defines satisfying_SIC WAYBEL35:def 7 :
theorem Th16:
theorem
:: deftheorem defines SetBelow WAYBEL35:def 8 :
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
:: deftheorem Def9 defines sup-closed WAYBEL35:def 9 :
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 :
theorem Th25:
theorem
theorem Th27:
theorem
theorem