let L be 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 ) )
let R be 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 ) )
let C be strict_chain of R; ( 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 ) )
set X = Strict_Chains (R,C);
A1:
field (RelIncl (Strict_Chains (R,C))) = Strict_Chains (R,C)
by WELLORD2:def 1;
thus A2:
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
let Y be
set ;
ORDERS_1:def 10 ( not Y c= Strict_Chains (R,C) or not (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order or ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) ) )
assume that A3:
Y c= Strict_Chains (
R,
C)
and A4:
(RelIncl (Strict_Chains (R,C))) |_2 Y is
being_linear-order
;
ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) )
per cases
( Y is empty or not Y is empty )
;
suppose A6:
not
Y is
empty
;
ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) )take Z =
union Y;
( Z in Strict_Chains (R,C) & ( for b1 being set holds
( not b1 in Y or [b1,Z] in RelIncl (Strict_Chains (R,C)) ) ) )
Z c= the
carrier of
L
then reconsider S =
Z as
Subset of
L ;
A9:
S is
strict_chain of
R
proof
(RelIncl (Strict_Chains (R,C))) |_2 Y is
connected
by A4;
then A10:
(RelIncl (Strict_Chains (R,C))) |_2 Y is_connected_in field ((RelIncl (Strict_Chains (R,C))) |_2 Y)
by RELAT_2:def 14;
A11:
(RelIncl (Strict_Chains (R,C))) |_2 Y = RelIncl Y
by A3, WELLORD2:7;
let x,
y be
set ;
WAYBEL35:def 3 ( x in S & y in S & not [x,y] in R & not x = y implies [y,x] in R )
A12:
field (RelIncl Y) = Y
by WELLORD2:def 1;
assume
x in S
;
( not y in S or [x,y] in R or x = y or [y,x] in R )
then consider A being
set such that A13:
x in A
and A14:
A in Y
by TARSKI:def 4;
A15:
A is
strict_chain of
R
by A3, A14, Def5;
assume
y in S
;
( [x,y] in R or x = y or [y,x] in R )
then consider B being
set such that A16:
y in B
and A17:
B in Y
by TARSKI:def 4;
A18:
B is
strict_chain of
R
by A3, A17, Def5;
per cases
( A <> B or A = B )
;
suppose
A <> B
;
( [x,y] in R or x = y or [y,x] in R )then
(
[A,B] in RelIncl Y or
[B,A] in RelIncl Y )
by A14, A17, A10, A11, A12, RELAT_2:def 6;
then
(
A c= B or
B c= A )
by A14, A17, WELLORD2:def 1;
hence
(
[x,y] in R or
x = y or
[y,x] in R )
by A13, A16, A15, A18, Def3;
verum end; end;
end;
C c= Z
hence A21:
Z in Strict_Chains (
R,
C)
by A9, Def5;
for b1 being set holds
( not b1 in Y or [b1,Z] in RelIncl (Strict_Chains (R,C)) )let y be
set ;
( not y in Y or [y,Z] in RelIncl (Strict_Chains (R,C)) )assume A22:
y in Y
;
[y,Z] in RelIncl (Strict_Chains (R,C))then
y c= Z
by ZFMISC_1:74;
hence
[y,Z] in RelIncl (Strict_Chains (R,C))
by A3, A21, A22, WELLORD2:def 1;
verum end; end;
end;
A23:
RelIncl (Strict_Chains (R,C)) is_transitive_in Strict_Chains (R,C)
by WELLORD2:20;
A24:
RelIncl (Strict_Chains (R,C)) is_antisymmetric_in Strict_Chains (R,C)
by WELLORD2:21;
RelIncl (Strict_Chains (R,C)) is_reflexive_in Strict_Chains (R,C)
by WELLORD2:19;
then
RelIncl (Strict_Chains (R,C)) partially_orders Strict_Chains (R,C)
by A23, A24;
then consider D being set such that
A25:
D is_maximal_in RelIncl (Strict_Chains (R,C))
by A1, A2, ORDERS_1:63;
take
D
; ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )
thus
D is_maximal_in RelIncl (Strict_Chains (R,C))
by A25; C c= D
D in field (RelIncl (Strict_Chains (R,C)))
by A25;
hence
C c= D
by A1, Def5; verum