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, y be object ; :: according to RELAT_2:def 7 :: 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, Def13;
A7: the InternalRel of A is_strongly_connected_in X by Def7;
A8: the InternalRel of A is_strongly_connected_in Y by Def7;

now :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

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

end;

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

now :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

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

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 Th42;
then X c= Y ;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A8; :: 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 Th42;
then Y c= X ;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A7; :: 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 Def7; :: thesis: verum