let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for R being auxiliary(iv) Relation of L

for C being strict_chain of R st C is maximal holds

Bottom L in C

let R be auxiliary(iv) Relation of L; :: thesis: for C being strict_chain of R st C is maximal holds

Bottom L in C

let C be strict_chain of R; :: thesis: ( C is maximal implies Bottom L in C )

assume A1: for D being strict_chain of R st C c= D holds

C = D ; :: according to WAYBEL35:def 4 :: thesis: Bottom L in C

C \/ {(Bottom L)} is strict_chain of R by Th5;

then A2: C \/ {(Bottom L)} = C by A1, XBOOLE_1:7;

assume not Bottom L in C ; :: thesis: contradiction

then not Bottom L in {(Bottom L)} by A2, XBOOLE_0:def 3;

hence contradiction by TARSKI:def 1; :: thesis: verum

for C being strict_chain of R st C is maximal holds

Bottom L in C

let R be auxiliary(iv) Relation of L; :: thesis: for C being strict_chain of R st C is maximal holds

Bottom L in C

let C be strict_chain of R; :: thesis: ( C is maximal implies Bottom L in C )

assume A1: for D being strict_chain of R st C c= D holds

C = D ; :: according to WAYBEL35:def 4 :: thesis: Bottom L in C

C \/ {(Bottom L)} is strict_chain of R by Th5;

then A2: C \/ {(Bottom L)} = C by A1, XBOOLE_1:7;

assume not Bottom L in C ; :: thesis: contradiction

then not Bottom L in {(Bottom L)} by A2, XBOOLE_0:def 3;

hence contradiction by TARSKI:def 1; :: thesis: verum