:: deftheorem Def1 defines Maximal_in ARMSTRNG:def 1 :
for X being set
for R being Relation
for b₃ being Subset of X holds
( b₃ = R Maximal_in X iff for x being object holds
( x in b₃ iff x is_maximal_wrt X,R ) );