let A be non empty Poset; ( ( 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
; 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 #);
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 ;
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 A4:
(
x in C &
y in C )
;
( [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;
hence
(
[x,y] in the
InternalRel of
A or
[y,x] in the
InternalRel of
A )
;
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
;
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 #);
( f in E implies f <= e )
reconsider b =
f as
Element of
A ;
assume
f in E
;
f <= e
then
a <= b
by A6;
then
[f,e] in R
by A2;
hence
f <= e
;
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
; for b being Element of A holds not b < d
let b be Element of A; not b < d
reconsider f = b as Element of RelStr(# the carrier of A,R #) ;
assume A8:
b < d
; contradiction
then
b <= d
;
then
[e,f] in R
by A2;
then
e <= f
;
then
e < f
by A8;
hence
contradiction
by A7; verum