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 7;
per cases ( [f,g] in the InternalRel of (ConPoset (P,P)) or [g,f] in the InternalRel of (ConPoset (P,P)) ) by A2, A1, RELAT_2:def 7;
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
A3: ( f = f1 & g = g1 & f1 <= g1 ) by Def7;
thus ( f <= g or g <= f ) by A3; :: 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
A4: ( g = g1 & f = f1 & g1 <= f1 ) by Def7;
thus ( f <= g or g <= f ) by A4; :: thesis: verum
end;
end;