let A be non empty Poset; :: thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of A
let f be Choice_Function of BOOL the carrier of A; :: thesis: union (Chains f) is Chain of A
reconsider C = union (Chains f) as Subset of A by Lm2;
the InternalRel of A is_strongly_connected_in C

proof

let x be set ; :: according to RELAT_2:def 7 :: thesis: for b₁ being set holds
( not x in C or not b₁ in C or [x,b₁] in the InternalRel of A or [b₁,x] in the InternalRel of A )
let y be set ; :: thesis: ( not x in C or not y in C or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume that
A1: x in C and
A2: y in C ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
consider X being set such that
A3: x in X and
A4: X in Chains f by A1, TARSKI:def 4;
consider Y being set such that
A5: y in Y and
A6: Y in Chains f by A2, TARSKI:def 4;
reconsider X = X, Y = Y as Chain of f by A4, A6, Def17;
A7: the InternalRel of A is_strongly_connected_in X by Def11;
A8: the InternalRel of A is_strongly_connected_in Y by Def11;

now

per cases ( X = Y or X <> Y ) ;

suppose X = Y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A7, RELAT_2:def 7; :: thesis: verum

end;

suppose A9: X <> Y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

now

per cases ( X is Initial_Segm of Y or Y is Initial_Segm of X ) by A9, Th83;

suppose X is Initial_Segm of Y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

then X c< Y by Th84;
then X c= Y by XBOOLE_0:def 8;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A8, RELAT_2:def 7; :: thesis: verum

end;

suppose Y is Initial_Segm of X ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

then Y c< X by Th84;
then Y c= X by XBOOLE_0:def 8;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A7, RELAT_2:def 7; :: thesis: verum

end;

end;

end;

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: thesis: verum

end;

end;

end;

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: thesis: verum

end;

hence union (Chains f) is Chain of A by Def11; :: thesis: verum