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 that
A1: a in {(Bottom L),x} and
A2: y in {(Bottom L),x} ; :: thesis: ( [a,y] in R or a = y or [y,a] in R )
A3: ( y = Bottom L or y = x ) by A2, TARSKI:def 2;
( a = Bottom L or a = x ) by A1, TARSKI:def 2;
hence ( [a,y] in R or a = y or [y,a] in R ) by A3, WAYBEL_4:def 6; :: thesis: verum