:: WAYBEL35 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for x, y, X being set holds
( not y in {x} \/ X or y = x or y in X )
proof end;

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

Lm2: for Y being trivial set
for A being Subset of Y holds A is trivial
proof end;

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

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

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

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

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

theorem Th1: :: WAYBEL35:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds RelIncl X is_reflexive_in X
proof end;

theorem Th2: :: WAYBEL35:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds RelIncl X is_transitive_in X
proof end;

theorem Th3: :: WAYBEL35:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds RelIncl X is_antisymmetric_in X
proof end;

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

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

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

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

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

:: 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) ) );

registration
let L be non empty RelStr ;
cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) Relation of the carrier of L,the carrier of L;
coherence
for b1 being Relation of L 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 L,the carrier of L;
coherence
for b1 being Relation of L st b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) holds
b1 is extra-order
by Def1;
end;

registration
let L be non empty RelStr ;
cluster auxiliary(iii) extra-order -> auxiliary extra-order Relation of the carrier of L,the carrier of L;
coherence
for b1 being Relation of L 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 L,the carrier of L;
coherence
for b1 being Relation of L st b1 is auxiliary holds
b1 is extra-order
proof end;
end;

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

definition
let L be lower-bounded with_suprema Poset;
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
ex b1 being Function of L,(InclPoset (LOWER L)) st
for x being Element of L holds b1 . x = R -below x
proof end;
uniqueness
for b1, b2 being Function of L,(InclPoset (LOWER L)) st ( for x being Element of L holds b1 . x = R -below x ) & ( for x being Element of L holds b2 . x = R -below x ) holds
b1 = b2
proof end;
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 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 );

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

definition
let L be 1-sorted ;
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
ex b1 being Subset of L st
for x, y being set st x in b1 & y in b1 & not [x,y] in R & not x = y holds
[y,x] in R
proof end;
end;

:: 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 Th4: :: WAYBEL35:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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

theorem Th5: :: WAYBEL35:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL35:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL35:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th8: :: WAYBEL35:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let L be 1-sorted ;
let R be Relation of the carrier of L;
let C be strict_chain of R;
attr C is maximal means :Def4: :: WAYBEL35:def 4
for D being strict_chain of R st C c= D holds
C = D;
end;

:: 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 );

definition
let L be 1-sorted ;
let R be Relation of the carrier of L;
let C be set ;
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
ex b1 being set st
for x being set holds
( x in b1 iff ( x is strict_chain of R & C c= x ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x is strict_chain of R & C c= x ) ) ) & ( for x being set holds
( x in b2 iff ( x is strict_chain of R & C c= x ) ) ) holds
b1 = b2
proof end;
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 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 ) ) );

registration
let L be 1-sorted ;
let R be Relation of the carrier of L;
let C be strict_chain of R;
cluster Strict_Chains R,C -> non empty ;
coherence
not Strict_Chains R,C is empty
by Def5;
end;

notation
let R be Relation;
let X be set ;
synonym X is_inductive_wrt R for X has_upper_Zorn_property_wrt R;
end;

theorem :: WAYBEL35:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th10: :: WAYBEL35:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

Lm3: 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;

theorem Th11: :: WAYBEL35:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL35:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: WAYBEL35:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL35:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL35:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let L be RelStr ;
let C be set ;
let R be Relation of the carrier of L;
pred R satisfies_SIC_on C means :Def6: :: WAYBEL35:def 6
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 );
end;

:: 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 ) );

definition
let L be RelStr ;
let R be Relation of the carrier of L;
let C be strict_chain of R;
attr C is satisfying_SIC means :Def7: :: WAYBEL35:def 7
R satisfies_SIC_on C;
end;

:: 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 );

notation
let L be RelStr ;
let R be Relation of the carrier of L;
let C be strict_chain of R;
synonym satisfying_the_interpolation_property C for satisfying_SIC CC satisfies_the_interpolation_propertysatisfies_the_interpolation_property ;
synonym C satisfies_the_interpolation_property for satisfying_SIC CC satisfies_the_interpolation_propertysatisfies_the_interpolation_property ;
end;

theorem Th16: :: WAYBEL35:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

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

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

theorem :: WAYBEL35:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let R be Relation;
let C, y be set ;
func SetBelow R,C,y -> set equals :: WAYBEL35:def 8
(R " {y}) /\ C;
coherence
(R " {y}) /\ C is set
;
end;

:: 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: :: WAYBEL35:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

definition
let L be 1-sorted ;
let R be Relation of the carrier of L;
let C, y be set ;
:: original: SetBelow
redefine func SetBelow R,C,y -> Subset of L;
coherence
SetBelow R,C,y is Subset of L
proof end;
end;

theorem Th19: :: WAYBEL35:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th20: :: WAYBEL35:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th21: :: WAYBEL35:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

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

:: 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: :: WAYBEL35:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: WAYBEL35:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: WAYBEL35:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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: :: WAYBEL35:def 10
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) )
proof end;
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
proof end;
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) ) );

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
proof end;
end;

theorem Th25: :: WAYBEL35:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL35:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th27: :: WAYBEL35:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL35:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL35:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;