:: WAYBEL35 semantic presentation

Lemma1: for b1, b2, b3 being set holds
( not b2 in {b1} \/ b3 or b2 = b1 or b2 in b3 )
proof end;

registration
let c1 be set ;
cluster trivial Element of bool a1;
existence
ex b1 being Subset of c1 st b1 is trivial
proof end;
end;

Lemma2: for b1 being trivial set
for b2 being Subset of b1 holds b2 is trivial
proof end;

registration
let c1 be trivial set ;
cluster -> trivial Element of bool a1;
coherence
for b1 being Subset of c1 holds b1 is trivial by Lemma2;
end;

registration
let c1 be 1-sorted ;
cluster trivial Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st b1 is trivial
proof end;
end;

registration
let c1 be RelStr ;
cluster trivial Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st b1 is trivial
proof end;
end;

registration
let c1 be non empty 1-sorted ;
cluster non empty trivial Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st
( not b1 is empty & b1 is trivial )
proof end;
end;

registration
let c1 be non empty RelStr ;
cluster non empty trivial Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st
( not b1 is empty & b1 is trivial )
proof end;
end;

theorem Th1: :: WAYBEL35:1
for b1 being set holds RelIncl b1 is_reflexive_in b1
proof end;

theorem Th2: :: WAYBEL35:2
for b1 being set holds RelIncl b1 is_transitive_in b1
proof end;

theorem Th3: :: WAYBEL35:3
for b1 being set holds RelIncl b1 is_antisymmetric_in b1
proof end;

registration
let c1 be RelStr ;
cluster auxiliary(i) Relation of the carrier of a1,the carrier of a1;
existence
ex b1 being Relation of c1 st b1 is auxiliary(i)
proof end;
end;

registration
let c1 be transitive RelStr ;
cluster auxiliary(i) auxiliary(ii) Relation of the carrier of a1,the carrier of a1;
existence
ex b1 being Relation of c1 st
( b1 is auxiliary(i) & b1 is auxiliary(ii) )
proof end;
end;

registration
let c1 be antisymmetric with_suprema RelStr ;
cluster auxiliary(iii) Relation of the carrier of a1,the carrier of a1;
existence
ex b1 being Relation of c1 st b1 is auxiliary(iii)
proof end;
end;

registration
let c1 be non empty antisymmetric lower-bounded RelStr ;
cluster auxiliary(iv) Relation of the carrier of a1,the carrier of a1;
existence
ex b1 being Relation of c1 st b1 is auxiliary(iv)
proof end;
end;

definition
let c1 be non empty RelStr ;
let c2 be Relation of c1;
attr a2 is extra-order means :Def1: :: WAYBEL35:def 1
( a2 is auxiliary(i) & a2 is auxiliary(ii) & a2 is auxiliary(iv) );
end;

:: deftheorem Def1 defines extra-order WAYBEL35:def 1 :
for b1 being non empty RelStr
for b2 being Relation of b1 holds
( b2 is extra-order iff ( b2 is auxiliary(i) & b2 is auxiliary(ii) & b2 is auxiliary(iv) ) );

registration
let c1 be non empty RelStr ;
cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) Relation of the carrier of a1,the carrier of a1;
coherence
for b1 being Relation of c1 st b1 is extra-order holds
( b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) ) by Def1;
cluster auxiliary(i) auxiliary(ii) auxiliary(iv) -> extra-order Relation of the carrier of a1,the carrier of a1;
coherence
for b1 being Relation of c1 st b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) holds
b1 is extra-order by Def1;
end;

registration
let c1 be non empty RelStr ;
cluster auxiliary(iii) extra-order -> auxiliary extra-order Relation of the carrier of a1,the carrier of a1;
coherence
for b1 being Relation of c1 st b1 is extra-order & b1 is auxiliary(iii) holds
b1 is auxiliary
proof end;
cluster auxiliary -> auxiliary(i) auxiliary(ii) auxiliary(iv) extra-order Relation of the carrier of a1,the carrier of a1;
coherence
for b1 being Relation of c1 st b1 is auxiliary holds
b1 is extra-order
proof end;
end;

registration
let c1 be non empty transitive antisymmetric lower-bounded RelStr ;
cluster auxiliary(i) auxiliary(ii) auxiliary(iv) extra-order Relation of the carrier of a1,the carrier of a1;
existence
ex b1 being Relation of c1 st b1 is extra-order
proof end;
end;

definition
let c1 be lower-bounded with_suprema Poset;
let c2 be auxiliary(ii) Relation of c1;
func c2 -LowerMap -> Function of a1,(InclPoset (LOWER a1)) means :Def2: :: WAYBEL35:def 2
for b1 being Element of a1 holds a3 . b1 = a2 -below b1;
existence
ex b1 being Function of c1,(InclPoset (LOWER c1)) st
for b2 being Element of c1 holds b1 . b2 = c2 -below b2
proof end;
uniqueness
for b1, b2 being Function of c1,(InclPoset (LOWER c1)) st ( for b3 being Element of c1 holds b1 . b3 = c2 -below b3 ) & ( for b3 being Element of c1 holds b2 . b3 = c2 -below b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines -LowerMap WAYBEL35:def 2 :
for b1 being lower-bounded with_suprema Poset
for b2 being auxiliary(ii) Relation of b1
for b3 being Function of b1,(InclPoset (LOWER b1)) holds
( b3 = b2 -LowerMap iff for b4 being Element of b1 holds b3 . b4 = b2 -below b4 );

registration
let c1 be lower-bounded with_suprema Poset;
let c2 be auxiliary(ii) Relation of c1;
cluster a2 -LowerMap -> monotone ;
coherence
c2 -LowerMap is monotone
proof end;
end;

definition
let c1 be 1-sorted ;
let c2 be Relation of the carrier of c1;
mode strict_chain of c2 -> Subset of a1 means :Def3: :: WAYBEL35:def 3
for b1, b2 being set st b1 in a3 & b2 in a3 & not [b1,b2] in a2 & not b1 = b2 holds
[b2,b1] in a2;
existence
ex b1 being Subset of c1 st
for b2, b3 being set st b2 in b1 & b3 in b1 & not [b2,b3] in c2 & not b2 = b3 holds
[b3,b2] in c2
proof end;
end;

:: deftheorem Def3 defines strict_chain WAYBEL35:def 3 :
for b1 being 1-sorted
for b2 being Relation of the carrier of b1
for b3 being Subset of b1 holds
( b3 is strict_chain of b2 iff for b4, b5 being set st b4 in b3 & b5 in b3 & not [b4,b5] in b2 & not b4 = b5 holds
[b5,b4] in b2 );

theorem Th4: :: WAYBEL35:4
for b1 being 1-sorted
for b2 being trivial Subset of b1
for b3 being Relation of the carrier of b1 holds b2 is strict_chain of b3
proof end;

registration
let c1 be non empty 1-sorted ;
let c2 be Relation of the carrier of c1;
cluster non empty trivial strict_chain of a2;
existence
ex b1 being strict_chain of c2 st
( not b1 is empty & b1 is trivial )
proof end;
end;

theorem Th5: :: WAYBEL35:5
for b1 being antisymmetric RelStr
for b2 being auxiliary(i) Relation of b1
for b3 being strict_chain of b2
for b4, b5 being Element of b1 st b4 in b3 & b5 in b3 & b4 < b5 holds
[b4,b5] in b2
proof end;

theorem Th6: :: WAYBEL35:6
for b1 being antisymmetric RelStr
for b2 being auxiliary(i) Relation of b1
for b3, b4 being Element of b1 st [b3,b4] in b2 & [b4,b3] in b2 holds
b3 = b4
proof end;

theorem Th7: :: WAYBEL35:7
for b1 being non empty antisymmetric lower-bounded RelStr
for b2 being Element of b1
for b3 being auxiliary(iv) Relation of b1 holds {(Bottom b1),b2} is strict_chain of b3
proof end;

theorem Th8: :: WAYBEL35:8
for b1 being non empty antisymmetric lower-bounded RelStr
for b2 being auxiliary(iv) Relation of b1
for b3 being strict_chain of b2 holds b3 \/ {(Bottom b1)} is strict_chain of b2
proof end;

definition
let c1 be 1-sorted ;
let c2 be Relation of the carrier of c1;
let c3 be strict_chain of c2;
attr a3 is maximal means :Def4: :: WAYBEL35:def 4
for b1 being strict_chain of a2 st a3 c= b1 holds
a3 = b1;
end;

:: deftheorem Def4 defines maximal WAYBEL35:def 4 :
for b1 being 1-sorted
for b2 being Relation of the carrier of b1
for b3 being strict_chain of b2 holds
( b3 is maximal iff for b4 being strict_chain of b2 st b3 c= b4 holds
b3 = b4 );

definition
let c1 be 1-sorted ;
let c2 be Relation of the carrier of c1;
let c3 be set ;
func Strict_Chains c2,c3 -> set means :Def5: :: WAYBEL35:def 5
for b1 being set holds
( b1 in a4 iff ( b1 is strict_chain of a2 & a3 c= b1 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 is strict_chain of c2 & c3 c= b2 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ( b3 is strict_chain of c2 & c3 c= b3 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 is strict_chain of c2 & c3 c= b3 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Strict_Chains WAYBEL35:def 5 :
for b1 being 1-sorted
for b2 being Relation of the carrier of b1
for b3 being set
for b4 being set holds
( b4 = Strict_Chains b2,b3 iff for b5 being set holds
( b5 in b4 iff ( b5 is strict_chain of b2 & b3 c= b5 ) ) );

registration
let c1 be 1-sorted ;
let c2 be Relation of the carrier of c1;
let c3 be strict_chain of c2;
cluster Strict_Chains a2,a3 -> non empty ;
coherence
not Strict_Chains c2,c3 is empty by Def5;
end;

notation
let c1 be Relation;
let c2 be set ;
synonym c2 is_inductive_wrt c1 for c2 has_upper_Zorn_property_wrt c1;
end;

theorem Th9: :: WAYBEL35:9
for b1 being 1-sorted
for b2 being Relation of the carrier of b1
for b3 being strict_chain of b2 holds
( Strict_Chains b2,b3 is_inductive_wrt RelIncl (Strict_Chains b2,b3) & ex b4 being set st
( b4 is_maximal_in RelIncl (Strict_Chains b2,b3) & b3 c= b4 ) )
proof end;

theorem Th10: :: WAYBEL35:10
for b1 being non empty transitive RelStr
for b2 being non empty Subset of b1
for b3 being Subset of b2 st ex_sup_of b3,b1 & "\/" b3,b1 in b2 holds
( ex_sup_of b3, subrelstr b2 & "\/" b3,b1 = "\/" b3,(subrelstr b2) )
proof end;

Lemma15: for b1 being non empty Poset
for b2 being auxiliary(i) auxiliary(ii) Relation of b1
for b3 being non empty strict_chain of b2
for b4 being Subset of b3 st ex_sup_of b4,b1 & b3 is maximal & not "\/" b4,b1 in b3 holds
ex b5 being Element of b1 st
( b5 in b3 & "\/" b4,b1 < b5 & not [("\/" b4,b1),b5] in b2 & ex b6 being Element of (subrelstr b3) st
( b5 = b6 & b4 is_<=_than b6 & ( for b7 being Element of (subrelstr b3) st b4 is_<=_than b7 holds
b6 <= b7 ) ) )
proof end;

theorem Th11: :: WAYBEL35:11
for b1 being non empty Poset
for b2 being auxiliary(i) auxiliary(ii) Relation of b1
for b3 being non empty strict_chain of b2
for b4 being Subset of b3 st ex_sup_of b4,b1 & b3 is maximal holds
ex_sup_of b4, subrelstr b3
proof end;

theorem Th12: :: WAYBEL35:12
for b1 being non empty Poset
for b2 being auxiliary(i) auxiliary(ii) Relation of b1
for b3 being non empty strict_chain of b2
for b4 being Subset of b3 st ex_inf_of (uparrow ("\/" b4,b1)) /\ b3,b1 & ex_sup_of b4,b1 & b3 is maximal holds
( "\/" b4,(subrelstr b3) = "/\" ((uparrow ("\/" b4,b1)) /\ b3),b1 & ( not "\/" b4,b1 in b3 implies "\/" b4,b1 < "/\" ((uparrow ("\/" b4,b1)) /\ b3),b1 ) )
proof end;

theorem Th13: :: WAYBEL35:13
for b1 being non empty complete Poset
for b2 being auxiliary(i) auxiliary(ii) Relation of b1
for b3 being non empty strict_chain of b2 st b3 is maximal holds
subrelstr b3 is complete
proof end;

theorem Th14: :: WAYBEL35:14
for b1 being non empty antisymmetric lower-bounded RelStr
for b2 being auxiliary(iv) Relation of b1
for b3 being strict_chain of b2 st b3 is maximal holds
Bottom b1 in b3
proof end;

theorem Th15: :: WAYBEL35:15
for b1 being non empty upper-bounded Poset
for b2 being auxiliary(ii) Relation of b1
for b3 being strict_chain of b2
for b4 being Element of b1 st b3 is maximal & b4 is_maximum_of b3 & [b4,(Top b1)] in b2 holds
( [(Top b1),(Top b1)] in b2 & b4 = Top b1 )
proof end;

definition
let c1 be RelStr ;
let c2 be set ;
let c3 be Relation of the carrier of c1;
pred c3 satisfies_SIC_on c2 means :Def6: :: WAYBEL35:def 6
for b1, b2 being Element of a1 st b1 in a2 & b2 in a2 & [b1,b2] in a3 & b1 <> b2 holds
ex b3 being Element of a1 st
( b3 in a2 & [b1,b3] in a3 & [b3,b2] in a3 & b1 <> b3 );
end;

:: deftheorem Def6 defines satisfies_SIC_on WAYBEL35:def 6 :
for b1 being RelStr
for b2 being set
for b3 being Relation of the carrier of b1 holds
( b3 satisfies_SIC_on b2 iff for b4, b5 being Element of b1 st b4 in b2 & b5 in b2 & [b4,b5] in b3 & b4 <> b5 holds
ex b6 being Element of b1 st
( b6 in b2 & [b4,b6] in b3 & [b6,b5] in b3 & b4 <> b6 ) );

definition
let c1 be RelStr ;
let c2 be Relation of the carrier of c1;
let c3 be strict_chain of c2;
attr a3 is satisfying_SIC means :Def7: :: WAYBEL35:def 7
a2 satisfies_SIC_on a3;
end;

:: deftheorem Def7 defines satisfying_SIC WAYBEL35:def 7 :
for b1 being RelStr
for b2 being Relation of the carrier of b1
for b3 being strict_chain of b2 holds
( b3 is satisfying_SIC iff b2 satisfies_SIC_on b3 );

notation
let c1 be RelStr ;
let c2 be Relation of the carrier of c1;
let c3 be strict_chain of c2;
synonym satisfying_the_interpolation_property c3 for satisfying_SIC c3c3 satisfies_the_interpolation_propertysatisfies_the_interpolation_property ;
synonym c3 satisfies_the_interpolation_property for satisfying_SIC c3c3 satisfies_the_interpolation_propertysatisfies_the_interpolation_property ;
end;

theorem Th16: :: WAYBEL35:16
for b1 being RelStr
for b2 being set
for b3 being auxiliary(i) Relation of b1 st b3 satisfies_SIC_on b2 holds
for b4, b5 being Element of b1 st b4 in b2 & b5 in b2 & [b4,b5] in b3 & b4 <> b5 holds
ex b6 being Element of b1 st
( b6 in b2 & [b4,b6] in b3 & [b6,b5] in b3 & b4 < b6 )
proof end;

registration
let c1 be RelStr ;
let c2 be Relation of the carrier of c1;
cluster trivial -> satisfying_SIC strict_chain of a2;
coherence
for b1 being strict_chain of c2 st b1 is trivial holds
b1 is satisfying_SIC
proof end;
end;

registration
let c1 be non empty RelStr ;
let c2 be Relation of the carrier of c1;
cluster non empty trivial satisfying_SIC strict_chain of a2;
existence
ex b1 being strict_chain of c2 st
( not b1 is empty & b1 is trivial )
proof end;
end;

theorem Th17: :: WAYBEL35:17
for b1 being lower-bounded with_suprema Poset
for b2 being auxiliary(i) auxiliary(ii) Relation of b1
for b3 being strict_chain of b2 st b3 is maximal & b2 is satisfying_SI holds
b2 satisfies_SIC_on b3
proof end;

definition
let c1 be Relation;
let c2, c3 be set ;
func SetBelow c1,c2,c3 -> set equals :: WAYBEL35:def 8
(a1 " {a3}) /\ a2;
coherence
(c1 " {c3}) /\ c2 is set ;
end;

:: deftheorem Def8 defines SetBelow WAYBEL35:def 8 :
for b1 being Relation
for b2, b3 being set holds SetBelow b1,b2,b3 = (b1 " {b3}) /\ b2;

theorem Th18: :: WAYBEL35:18
for b1 being Relation
for b2, b3, b4 being set holds
( b3 in SetBelow b1,b2,b4 iff ( [b3,b4] in b1 & b3 in b2 ) )
proof end;

definition
let c1 be 1-sorted ;
let c2 be Relation of the carrier of c1;
let c3, c4 be set ;
redefine func SetBelow as SetBelow c2,c3,c4 -> Subset of a1;
coherence
SetBelow c2,c3,c4 is Subset of c1
proof end;
end;

theorem Th19: :: WAYBEL35:19
for b1 being RelStr
for b2 being auxiliary(i) Relation of b1
for b3 being set
for b4 being Element of b1 holds SetBelow b2,b3,b4 is_<=_than b4
proof end;

theorem Th20: :: WAYBEL35:20
for b1 being reflexive transitive RelStr
for b2 being auxiliary(ii) Relation of b1
for b3 being Subset of b1
for b4, b5 being Element of b1 st b4 <= b5 holds
SetBelow b2,b3,b4 c= SetBelow b2,b3,b5
proof end;

theorem Th21: :: WAYBEL35:21
for b1 being RelStr
for b2 being auxiliary(i) Relation of b1
for b3 being set
for b4 being Element of b1 st b4 in b3 & [b4,b4] in b2 & ex_sup_of SetBelow b2,b3,b4,b1 holds
b4 = sup (SetBelow b2,b3,b4)
proof end;

definition
let c1 be RelStr ;
let c2 be Subset of c1;
attr a2 is sup-closed means :Def9: :: WAYBEL35:def 9
for b1 being Subset of a2 st ex_sup_of b1,a1 holds
"\/" b1,a1 = "\/" b1,(subrelstr a2);
end;

:: deftheorem Def9 defines sup-closed WAYBEL35:def 9 :
for b1 being RelStr
for b2 being Subset of b1 holds
( b2 is sup-closed iff for b3 being Subset of b2 st ex_sup_of b3,b1 holds
"\/" b3,b1 = "\/" b3,(subrelstr b2) );

theorem Th22: :: WAYBEL35:22
for b1 being non empty complete Poset
for b2 being extra-order Relation of b1
for b3 being satisfying_SIC strict_chain of b2
for b4, b5 being Element of b1 st b4 in b3 & b5 in b3 & b4 < b5 holds
ex b6 being Element of b1 st
( b4 < b6 & [b6,b5] in b2 & b6 = sup (SetBelow b2,b3,b6) )
proof end;

theorem Th23: :: WAYBEL35:23
for b1 being non empty lower-bounded Poset
for b2 being extra-order Relation of b1
for b3 being non empty strict_chain of b2 st b3 is sup-closed & ( for b4 being Element of b1 st b4 in b3 holds
ex_sup_of SetBelow b2,b3,b4,b1 ) & b2 satisfies_SIC_on b3 holds
for b4 being Element of b1 st b4 in b3 holds
b4 = sup (SetBelow b2,b3,b4)
proof end;

theorem Th24: :: WAYBEL35:24
for b1 being non empty reflexive antisymmetric RelStr
for b2 being auxiliary(i) Relation of b1
for b3 being strict_chain of b2 st ( for b4 being Element of b1 st b4 in b3 holds
( ex_sup_of SetBelow b2,b3,b4,b1 & b4 = sup (SetBelow b2,b3,b4) ) ) holds
b2 satisfies_SIC_on b3
proof end;

definition
let c1 be non empty RelStr ;
let c2 be Relation of the carrier of c1;
let c3 be set ;
func SupBelow c2,c3 -> set means :Def10: :: WAYBEL35:def 10
for b1 being set holds
( b1 in a4 iff b1 = sup (SetBelow a2,a3,b1) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 = sup (SetBelow c2,c3,b2) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 = sup (SetBelow c2,c3,b3) ) ) & ( for b3 being set holds
( b3 in b2 iff b3 = sup (SetBelow c2,c3,b3) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines SupBelow WAYBEL35:def 10 :
for b1 being non empty RelStr
for b2 being Relation of the carrier of b1
for b3 being set
for b4 being set holds
( b4 = SupBelow b2,b3 iff for b5 being set holds
( b5 in b4 iff b5 = sup (SetBelow b2,b3,b5) ) );

definition
let c1 be non empty RelStr ;
let c2 be Relation of the carrier of c1;
let c3 be set ;
redefine func SupBelow as SupBelow c2,c3 -> Subset of a1;
coherence
SupBelow c2,c3 is Subset of c1
proof end;
end;

theorem Th25: :: WAYBEL35:25
for b1 being non empty reflexive transitive RelStr
for b2 being auxiliary(i) auxiliary(ii) Relation of b1
for b3 being strict_chain of b2 st ( for b4 being Element of b1 holds ex_sup_of SetBelow b2,b3,b4,b1 ) holds
SupBelow b2,b3 is strict_chain of b2
proof end;

theorem Th26: :: WAYBEL35:26
for b1 being non empty Poset
for b2 being auxiliary(i) auxiliary(ii) Relation of b1
for b3 being Subset of b1 st ( for b4 being Element of b1 holds ex_sup_of SetBelow b2,b3,b4,b1 ) holds
SupBelow b2,b3 is sup-closed
proof end;

theorem Th27: :: WAYBEL35:27
for b1 being non empty complete Poset
for b2 being extra-order Relation of b1
for b3 being satisfying_SIC strict_chain of b2
for b4 being Element of b1 st b4 in SupBelow b2,b3 holds
b4 = "\/" { b5 where B is Element of b1 : ( b5 in SupBelow b2,b3 & [b5,b4] in b2 ) } ,b1
proof end;

theorem Th28: :: WAYBEL35:28
for b1 being non empty complete Poset
for b2 being extra-order Relation of b1
for b3 being satisfying_SIC strict_chain of b2 holds b2 satisfies_SIC_on SupBelow b2,b3
proof end;

theorem Th29: :: WAYBEL35:29
for b1 being non empty complete Poset
for b2 being extra-order Relation of b1
for b3 being satisfying_SIC strict_chain of b2
for b4, b5 being Element of b1 st b4 in b3 & b5 in b3 & b4 < b5 holds
ex b6 being Element of b1 st
( b6 in SupBelow b2,b3 & b4 < b6 & [b6,b5] in b2 )
proof end;