let A be non empty Poset; :: thesis: ( ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ) implies ex a being Element of A st
for b being Element of A holds not b < a )
set X = the carrier of A;
set R = the InternalRel of A ~ ;
A1: dom ( the InternalRel of A ~) = dom the InternalRel of A by RELAT_2:12
.= the carrier of A by PARTFUN1:def 2 ;
A2: for a, b being Element of A holds
( [a,b] in the InternalRel of A ~ iff b <= a ) by RELAT_1:def 7;
reconsider R = the InternalRel of A ~ as Order of the carrier of A by A1, PARTFUN1:def 2;
set B = RelStr(# the carrier of A,R #);
assume A3: for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ; :: thesis: ex a being Element of A st
for b being Element of A holds not b < a
for E being Chain of RelStr(# the carrier of A,R #) ex e being Element of RelStr(# the carrier of A,R #) st
for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e

proof

let E be Chain of RelStr(# the carrier of A,R #); :: thesis: ex e being Element of RelStr(# the carrier of A,R #) st
for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e
reconsider C = E as Subset of A ;
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 A4: ( x in C & y in C ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then reconsider e = x, f = y as Element of RelStr(# the carrier of A,R #) ;
reconsider e1 = e, f1 = f as Element of A ;
A5: ( e <= f or f <= e ) by A4, Th11;

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

per cases ( [e,f] in R or [f,e] in R ) by A5;

suppose [e,f] in R ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

then f1 <= e1 by A2;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: thesis: verum

end;

suppose [f,e] in R ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

then e1 <= f1 by A2;
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;

then reconsider C = C as Chain of A by Def7;
consider a being Element of A such that
A6: for b being Element of A st b in C holds
a <= b by A3;
reconsider e = a as Element of RelStr(# the carrier of A,R #) ;
take e ; :: thesis: for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e
let f be Element of RelStr(# the carrier of A,R #); :: thesis: ( f in E implies f <= e )
reconsider b = f as Element of A ;
assume f in E ; :: thesis: f <= e
then a <= b by A6;
then [f,e] in R by A2;
hence f <= e ; :: thesis: verum

end;

then consider e being Element of RelStr(# the carrier of A,R #) such that
A7: for f being Element of RelStr(# the carrier of A,R #) holds not e < f by Th55;
reconsider d = e as Element of A ;
take d ; :: thesis: for b being Element of A holds not b < d
let b be Element of A; :: thesis: not b < d
reconsider f = b as Element of RelStr(# the carrier of A,R #) ;
assume A8: b < d ; :: thesis: contradiction
then b <= d ;
then [e,f] in R by A2;
then e <= f ;
then e < f by A8;
hence contradiction by A7; :: thesis: verum