begin
:: deftheorem defines reflexive YELLOW_0:def 1 :
:: deftheorem defines transitive YELLOW_0:def 2 :
:: deftheorem defines antisymmetric YELLOW_0:def 3 :
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
begin
:: deftheorem Def4 defines lower-bounded YELLOW_0:def 4 :
:: deftheorem Def5 defines upper-bounded YELLOW_0:def 5 :
:: deftheorem defines bounded YELLOW_0:def 6 :
theorem
:: deftheorem Def7 defines ex_sup_of YELLOW_0:def 7 :
:: deftheorem Def8 defines ex_inf_of YELLOW_0:def 8 :
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem
definition
let L be
RelStr ;
let X be
set ;
func "\/" X,
L -> Element of
means :
Def9:
(
X is_<=_than it & ( for
a being
Element of st
X is_<=_than a holds
it <= a ) )
if ex_sup_of X,
L;
uniqueness
for b1, b2 being Element of st ex_sup_of X,L & X is_<=_than b1 & ( for a being Element of st X is_<=_than a holds
b1 <= a ) & X is_<=_than b2 & ( for a being Element of st X is_<=_than a holds
b2 <= a ) holds
b1 = b2
existence
( ex_sup_of X,L implies ex b1 being Element of st
( X is_<=_than b1 & ( for a being Element of st X is_<=_than a holds
b1 <= a ) ) )
correctness
consistency
for b1 being Element of holds verum;
;
func "/\" X,
L -> Element of
means :
Def10:
(
X is_>=_than it & ( for
a being
Element of st
X is_>=_than a holds
a <= it ) )
if ex_inf_of X,
L;
uniqueness
for b1, b2 being Element of st ex_inf_of X,L & X is_>=_than b1 & ( for a being Element of st X is_>=_than a holds
a <= b1 ) & X is_>=_than b2 & ( for a being Element of st X is_>=_than a holds
a <= b2 ) holds
b1 = b2
existence
( ex_inf_of X,L implies ex b1 being Element of st
( X is_>=_than b1 & ( for a being Element of st X is_>=_than a holds
a <= b1 ) ) )
correctness
consistency
for b1 being Element of holds verum;
;
end;
:: deftheorem Def9 defines "\/" YELLOW_0:def 9 :
:: deftheorem Def10 defines "/\" YELLOW_0:def 10 :
theorem
theorem
theorem
theorem
theorem Th30:
theorem Th31:
theorem
theorem
theorem Th34:
theorem Th35:
theorem
theorem
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
:: deftheorem defines Bottom YELLOW_0:def 11 :
:: deftheorem defines Top YELLOW_0:def 12 :
theorem
theorem
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def13 defines SubRelStr YELLOW_0:def 13 :
:: deftheorem Def14 defines full YELLOW_0:def 14 :
theorem
canceled;
theorem Th57:
theorem Th58:
:: deftheorem defines subrelstr YELLOW_0:def 15 :
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
:: deftheorem Def16 defines meet-inheriting YELLOW_0:def 16 :
:: deftheorem Def17 defines join-inheriting YELLOW_0:def 17 :
:: deftheorem defines infs-inheriting YELLOW_0:def 18 :
:: deftheorem defines sups-inheriting YELLOW_0:def 19 :
theorem Th64:
theorem Th65:
theorem
for
L being non
empty transitive RelStr for
S being non
empty full SubRelStr of
L for
x,
y being
Element of st
ex_inf_of {x,y},
L &
"/\" {x,y},
L in the
carrier of
S holds
(
ex_inf_of {x,y},
S &
"/\" {x,y},
S = "/\" {x,y},
L )
by Th64;
theorem
for
L being non
empty transitive RelStr for
S being non
empty full SubRelStr of
L for
x,
y being
Element of st
ex_sup_of {x,y},
L &
"\/" {x,y},
L in the
carrier of
S holds
(
ex_sup_of {x,y},
S &
"\/" {x,y},
S = "\/" {x,y},
L )
by Th65;
theorem
theorem
theorem
theorem