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;

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 :: thesis: not m <> Top L

hence
( [(Top L),(Top L)] in R & m = Top L )
by A3; :: thesis: verumA5:
m <= Top L
by YELLOW_0:45;

assume A6: m <> Top L ; :: thesis: contradiction

A7: {(Top L)} c= C \/ {(Top L)} by XBOOLE_1:7;

A8: ex_sup_of C,L by A2;

A9: sup C = m by A2;

C \/ {(Top L)} is strict_chain of R

Top L in {(Top L)} by TARSKI:def 1;

then Top L <= sup C by A7, A8, A17, YELLOW_4:1;

hence contradiction by A6, A5, A9, ORDERS_2:2; :: thesis: verum

end;assume A6: m <> Top L ; :: thesis: contradiction

A7: {(Top L)} c= C \/ {(Top L)} by XBOOLE_1:7;

A8: ex_sup_of C,L by A2;

A9: sup C = m by A2;

C \/ {(Top L)} is strict_chain of R

proof

then A17:
C \/ {(Top L)} = C
by A1, A4;
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 that

A10: a in C \/ {(Top L)} and

A11: b in C \/ {(Top L)} ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

A12: Top L <= Top L ;

end;assume that

A10: a in C \/ {(Top L)} and

A11: b in C \/ {(Top L)} ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

A12: 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 A10, A11, Lm1;

end;

suppose that A13:
a = Top L
and

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

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

reconsider b = b as Element of L by A14;

b <= sup C by A8, A14, YELLOW_4:1;

hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A9, A12, A13, WAYBEL_4:def 4; :: thesis: verum

end;b <= sup C by A8, A14, YELLOW_4:1;

hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A9, A12, A13, WAYBEL_4:def 4; :: thesis: verum

Top L in {(Top L)} by TARSKI:def 1;

then Top L <= sup C by A7, A8, A17, YELLOW_4:1;

hence contradiction by A6, A5, A9, ORDERS_2:2; :: thesis: verum