let P be non empty strict chain-complete Poset; :: thesis: 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)); :: thesis: 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; :: thesis: ( f in G & g in G & not f <= g implies g <= f )
assume A1: ( f in G & g in G ) ; :: thesis: ( 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 11;

per cases ( [f,g] in the InternalRel of (ConPoset (P,P)) or [g,f] in the InternalRel of (ConPoset (P,P)) ) by A2, RELAT_2:def 7, A1;

suppose [f,g] in the InternalRel of (ConPoset (P,P)) ; :: thesis: ( f <= g or g <= f )

then consider f1, g1 being Function of P,P such that
B1: ( f = f1 & g = g1 & f1 <= g1 ) by DefConRelat;
thus ( f <= g or g <= f ) by B1; :: thesis: verum

end;

suppose [g,f] in the InternalRel of (ConPoset (P,P)) ; :: thesis: ( f <= g or g <= f )

then consider g1, f1 being Function of P,P such that
B2: ( g = g1 & f = f1 & g1 <= f1 ) by DefConRelat;
thus ( f <= g or g <= f ) by B2; :: thesis: verum

end;

end;