let A be non empty Poset; 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); 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 ;
RELAT_2:def 7 ( 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
;
( [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;
hence
(
[x,y] in the
InternalRel of
A or
[y,x] in the
InternalRel of
A )
;
verum
end;
hence
union (Chains f) is Chain of A
by Def7; verum