let L be non empty antisymmetric lower-bounded RelStr ; 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; 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; {(Bottom L),x} is strict_chain of R
let a, y be set ; WAYBEL35:def 3 ( 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}
; ( [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; verum