:: deftheorem DefPA defines positive_alliance ROUGHS_3:def 8 :
for R being non empty RelStr holds
( R is positive_alliance iff the InternalRel of R is_positive_alliance_in the carrier of R );