let L be non empty upper-bounded Poset; :: thesis: for R being auxiliary(ii) Relation of L
for C being strict_chain of R
for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds
( [(Top L),(Top L)] in R & m = Top L )
let R be auxiliary(ii) Relation of L; :: thesis: for C being strict_chain of R
for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds
( [(Top L),(Top L)] in R & m = Top L )
let C be strict_chain of R; :: thesis: for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds
( [(Top L),(Top L)] in R & m = Top L )
let m be Element of L; :: thesis: ( C is maximal & m is_maximum_of C & [m,(Top L)] in R implies ( [(Top L),(Top L)] in R & m = Top L ) )
assume that
A1: C is maximal and
A2: m is_maximum_of C and
A3: [m,(Top L)] in R ; :: thesis: ( [(Top L),(Top L)] in R & m = Top L )
A4: C c= C \/ {(Top L)} by XBOOLE_1:7;

now

assume A5: m <> Top L ; :: thesis: contradiction
A6: m <= Top L by YELLOW_0:45;
A7: sup C = m by A2, WAYBEL_1:def 7;
A8: ex_sup_of C,L by A2, WAYBEL_1:def 7;
C \/ {(Top L)} is strict_chain of R

proof

let a, b be set ; :: according to WAYBEL35:def 3 :: thesis: ( a in C \/ {(Top L)} & b in C \/ {(Top L)} & not [a,b] in R & not a = b implies [b,a] in R )
assume A9: ( a in C \/ {(Top L)} & b in C \/ {(Top L)} ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )
A10: Top L <= Top L ;

per cases ( ( a in C & b in C ) or ( a = Top L & b in C ) or ( a in C & b = Top L ) or ( a = Top L & b = Top L ) ) by A9, Lm1;

suppose ( a in C & b in C ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) by Def3; :: thesis: verum

end;

suppose that A11: a = Top L and
A12: b in C ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

reconsider b = b as Element of L by A12;
b <= sup C by A8, A12, YELLOW_4:1;
hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A7, A10, A11, WAYBEL_4:def 5; :: thesis: verum

end;

suppose that A13: a in C and
A14: b = Top L ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

reconsider a = a as Element of L by A13;
a <= sup C by A8, A13, YELLOW_4:1;
hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A7, A10, A14, WAYBEL_4:def 5; :: thesis: verum

end;

suppose ( a = Top L & b = Top L ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) ; :: thesis: verum

end;

end;

end;

then A15: C \/ {(Top L)} = C by A1, A4, Def4;
A16: Top L in {(Top L)} by TARSKI:def 1;
{(Top L)} c= C \/ {(Top L)} by XBOOLE_1:7;
then Top L <= sup C by A8, A15, A16, YELLOW_4:1;
hence contradiction by A5, A6, A7, ORDERS_2:25; :: thesis: verum

end;

hence ( [(Top L),(Top L)] in R & m = Top L ) by A3; :: thesis: verum