let P be non empty strict chain-complete Poset; for G being non empty Chain of (ConPoset (P,P))
for f, g being monotone Function of P,P st f in G & g in G & not f <= g holds
g <= f
let G be non empty Chain of (ConPoset (P,P)); for f, g being monotone Function of P,P st f in G & g in G & not f <= g holds
g <= f
let f, g be monotone Function of P,P; ( f in G & g in G & not f <= g implies g <= f )
assume A1:
( f in G & g in G )
; ( f <= g or g <= f )
set S = the InternalRel of (ConPoset (P,P));
A2:
the InternalRel of (ConPoset (P,P)) is_strongly_connected_in G
by ORDERS_2:def 7;