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 )
assume A1: 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
set X = the carrier of A;
set R = the InternalRel of A ~ ;
A2: for a, b being Element of A holds
( [a,b] in the InternalRel of A ~ iff b <= a )

proof

let a, b be Element of A; :: thesis: ( [a,b] in the InternalRel of A ~ iff b <= a )
( [a,b] in the InternalRel of A ~ iff [b,a] in the InternalRel of A ) by RELAT_1:def 7;
hence ( [a,b] in the InternalRel of A ~ iff b <= a ) by Def9; :: thesis: verum

end;

dom (the InternalRel of A ~ ) = dom the InternalRel of A by RELAT_2:29
.= the carrier of A by PARTFUN1:def 4 ;
then reconsider R = the InternalRel of A ~ as Order of the carrier of A by PARTFUN1:def 4, RELAT_2:27, RELAT_2:40, RELAT_2:42;
set B = RelStr(# the carrier of A,R #);
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 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 A3: ( 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 #) ;
A4: ( ( e <= f or f <= e ) & R = the InternalRel of RelStr(# the carrier of A,R #) ) by A3, Th38;
reconsider e1 = e, f1 = f as Element of A ;

now

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

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 ) by Def9; :: 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 ) by Def9; :: 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 Def11;
consider a being Element of A such that
A5: for b being Element of A st b in C holds
a <= b by A1;
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 A5;
then ( [f,e] in R & R = the InternalRel of RelStr(# the carrier of A,R #) ) by A2;
hence f <= e by Def9; :: thesis: verum

end;

then consider e being Element of RelStr(# the carrier of A,R #) such that
A6: for f being Element of RelStr(# the carrier of A,R #) holds not e < f by Th162;
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 A7: b < d ; :: thesis: contradiction
then b <= d by Def10;
then ( [e,f] in R & R = the InternalRel of RelStr(# the carrier of A,R #) ) by A2;
then ( e <= f & b <> d ) by A7, Def9;
then e < f by Def10;
hence contradiction by A6; :: thesis: verum