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 :: thesis: not m <> Top L
A5: 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
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 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;
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 A13: a = Top L and
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;
suppose that A15: a in C and
A16: b = Top L ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )
reconsider a = a as Element of L by A15;
a <= sup C by A8, A15, YELLOW_4:1;
hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A9, A12, A16, WAYBEL_4:def 4; :: 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 A17: C \/ {(Top L)} = C by A1, A4;
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;
hence ( [(Top L),(Top L)] in R & m = Top L ) by A3; :: thesis: verum