:: deftheorem Def5 defines Strict_Chains WAYBEL35:def 5 :
for L being 1-sorted
for R being Relation of the carrier of L
for C, b₄ being set holds
( b₄ = Strict_Chains (R,C) iff for x being set holds
( x in b₄ iff ( x is strict_chain of R & C c= x ) ) );