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;

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;

suppose ( x in C & y in C ) ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )

hence ( [x,y] in R or x = y or [y,x] in R ) by Def3; :: thesis: verum

end;

suppose ( x in C & y = Bottom L ) ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )

hence ( [x,y] in R or x = y or [y,x] in R ) by WAYBEL_4:def 6; :: thesis: verum

end;

suppose ( x = Bottom L & y in C ) ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )

hence ( [x,y] in R or x = y or [y,x] in R ) by WAYBEL_4:def 6; :: thesis: verum

end;

suppose ( x = Bottom L & y = Bottom L ) ; :: thesis: ( [x,y] in R or x = y or [y,x] in R )

hence ( [x,y] in R or x = y or [y,x] in R ) ; :: thesis: verum

end;

end;