:: deftheorem Def3 defines strict_chain WAYBEL35:def 3 :
for L being 1-sorted
for R being Relation of the carrier of L
for b₃ being Subset of L holds
( b₃ is strict_chain of R iff for x, y being set st x in b₃ & y in b₃ & not [x,y] in R & not x = y holds
[y,x] in R );