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

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