:: deftheorem Def17 defines MinElement BAGORDER:def 17 :
for R being non empty connected RelStr
for C being non empty set st R is well_founded & C c= the carrier of R holds
for b₃ being Element of R holds
( b₃ = MinElement (C,R) iff ( b₃ in C & b₃ is_minimal_wrt C, the InternalRel of R ) );