:: deftheorem Def13 defines PosetMax BAGORDER:def 13 :
for R being non empty connected Poset
for X being Element of Fin the carrier of R st not X is empty holds
for b₃ being Element of R holds
( b₃ = PosetMax X iff ( b₃ in X & b₃ is_maximal_wrt X, the InternalRel of R ) );