let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for x being Element of L
for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R
let x be Element of L; :: thesis: for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R
let R be auxiliary(iv) Relation of L; :: thesis: {(Bottom L),x} is strict_chain of R
let a, y be set ; :: according to WAYBEL35:def 3 :: thesis: ( a in {(Bottom L),x} & y in {(Bottom L),x} & not [a,y] in R & not a = y implies [y,a] in R )
assume ( a in {(Bottom L),x} & y in {(Bottom L),x} ) ; :: thesis: ( [a,y] in R or a = y or [y,a] in R )
then ( ( a = Bottom L or a = x ) & ( y = Bottom L or y = x ) ) by TARSKI:def 2;
hence ( [a,y] in R or a = y or [y,a] in R ) by WAYBEL_4:def 7; :: thesis: verum