:: deftheorem Def4 defines well_founded-Part WELLFND1:def 4 :
for R being RelStr
for b₂ being Subset of R holds
( b₂ = well_founded-Part R iff b₂ = union { S where S is Subset of R : ( S is well_founded & S is lower ) } );