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 holds C \/ {(Bottom L)} is strict_chain of R

let R be auxiliary(iv) Relation of L; :: thesis: for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R

let C be strict_chain of R; :: thesis: C \/ {(Bottom L)} is strict_chain of R

set A = C \/ {(Bottom L)};

let x, y be set ; :: according to WAYBEL35:def 3 :: thesis: ( x in C \/ {(Bottom L)} & y in C \/ {(Bottom L)} & not [x,y] in R & not x = y implies [y,x] in R )

assume that

A1: x in C \/ {(Bottom L)} and

A2: y in C \/ {(Bottom L)} ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )

reconsider x = x, y = y as Element of L by A1, A2;

for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R

let R be auxiliary(iv) Relation of L; :: thesis: for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R

let C be strict_chain of R; :: thesis: C \/ {(Bottom L)} is strict_chain of R

set A = C \/ {(Bottom L)};

let x, y be set ; :: according to WAYBEL35:def 3 :: thesis: ( x in C \/ {(Bottom L)} & y in C \/ {(Bottom L)} & not [x,y] in R & not x = y implies [y,x] in R )

assume that

A1: x in C \/ {(Bottom L)} and

A2: y in C \/ {(Bottom L)} ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )

reconsider x = x, y = y as Element of L by A1, A2;

per cases
( ( x in C & y in C ) or ( x in C & y = Bottom L ) or ( x = Bottom L & y in C ) or ( x = Bottom L & y = Bottom L ) )
by A1, A2, Lm1;

end;