let L be 1-sorted ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) :: thesis: ex D being set st

( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )

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 ; :: thesis: ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )

thus D is_maximal_in RelIncl (Strict_Chains (R,C)) by A25; :: thesis: C c= D

D in field (RelIncl (Strict_Chains (R,C))) by A25;

hence C c= D by A1, Def5; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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)) :: thesis: ex D being set st

( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )

proof

A23:
RelIncl (Strict_Chains (R,C)) is_transitive_in Strict_Chains (R,C)
by WELLORD2:20;
let Y be set ; :: according to ORDERS_1:def 10 :: thesis: ( not Y c= Strict_Chains (R,C) or not (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order or ex b_{1} being set st

( b_{1} in Strict_Chains (R,C) & ( for b_{2} being set holds

( not b_{2} in Y or [b_{2},b_{1}] 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 ; :: thesis: ex b_{1} being set st

( b_{1} in Strict_Chains (R,C) & ( for b_{2} being set holds

( not b_{2} in Y or [b_{2},b_{1}] in RelIncl (Strict_Chains (R,C)) ) ) )

end;( b

( not b

assume that

A3: Y c= Strict_Chains (R,C) and

A4: (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order ; :: thesis: ex b

( b

( not b

per cases
( Y is empty or not Y is empty )
;

end;

suppose A5:
Y is empty
; :: thesis: ex b_{1} being set st

( b_{1} in Strict_Chains (R,C) & ( for b_{2} being set holds

( not b_{2} in Y or [b_{2},b_{1}] in RelIncl (Strict_Chains (R,C)) ) ) )

( b

( not b

take
C
; :: thesis: ( C in Strict_Chains (R,C) & ( for b_{1} being set holds

( not b_{1} in Y or [b_{1},C] in RelIncl (Strict_Chains (R,C)) ) ) )

thus ( C in Strict_Chains (R,C) & ( for b_{1} being set holds

( not b_{1} in Y or [b_{1},C] in RelIncl (Strict_Chains (R,C)) ) ) )
by A5, Def5; :: thesis: verum

end;( not b

thus ( C in Strict_Chains (R,C) & ( for b

( not b

suppose A6:
not Y is empty
; :: thesis: ex b_{1} being set st

( b_{1} in Strict_Chains (R,C) & ( for b_{2} being set holds

( not b_{2} in Y or [b_{2},b_{1}] in RelIncl (Strict_Chains (R,C)) ) ) )

( b

( not b

take Z = union Y; :: thesis: ( Z in Strict_Chains (R,C) & ( for b_{1} being set holds

( not b_{1} in Y or [b_{1},Z] in RelIncl (Strict_Chains (R,C)) ) ) )

Z c= the carrier of L

A9: S is strict_chain of R_{1} being set holds

( not b_{1} in Y or [b_{1},Z] in RelIncl (Strict_Chains (R,C)) )

let y be set ; :: thesis: ( not y in Y or [y,Z] in RelIncl (Strict_Chains (R,C)) )

assume A22: y in Y ; :: thesis: [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; :: thesis: verum

end;( not b

Z c= the carrier of L

proof

then reconsider S = Z as Subset of L ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in the carrier of L )

assume z in Z ; :: thesis: z in the carrier of L

then consider A being set such that

A7: z in A and

A8: A in Y by TARSKI:def 4;

A is strict_chain of R by A3, A8, Def5;

hence z in the carrier of L by A7; :: thesis: verum

end;assume z in Z ; :: thesis: z in the carrier of L

then consider A being set such that

A7: z in A and

A8: A in Y by TARSKI:def 4;

A is strict_chain of R by A3, A8, Def5;

hence z in the carrier of L by A7; :: thesis: verum

A9: S is strict_chain of R

proof

C c= Z
(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 ; :: according to WAYBEL35:def 3 :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( [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;

end;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 ; :: according to WAYBEL35:def 3 :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( [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 )
;

end;

suppose
A <> B
; :: thesis: ( [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; :: thesis: verum

end;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; :: thesis: verum

proof

hence A21:
Z in Strict_Chains (R,C)
by A9, Def5; :: thesis: for b
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in Z )

assume A19: c in C ; :: thesis: c in Z

consider y being object such that

A20: y in Y by A6;

reconsider y = y as set by TARSKI:1;

C c= y by A3, A20, Def5;

hence c in Z by A19, A20, TARSKI:def 4; :: thesis: verum

end;assume A19: c in C ; :: thesis: c in Z

consider y being object such that

A20: y in Y by A6;

reconsider y = y as set by TARSKI:1;

C c= y by A3, A20, Def5;

hence c in Z by A19, A20, TARSKI:def 4; :: thesis: verum

( not b

let y be set ; :: thesis: ( not y in Y or [y,Z] in RelIncl (Strict_Chains (R,C)) )

assume A22: y in Y ; :: thesis: [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; :: thesis: verum

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 ; :: thesis: ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )

thus D is_maximal_in RelIncl (Strict_Chains (R,C)) by A25; :: thesis: C c= D

D in field (RelIncl (Strict_Chains (R,C))) by A25;

hence C c= D by A1, Def5; :: thesis: verum