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