:: deftheorem defines alliance ROUGHS_3:def 10 :
for R being non empty RelStr holds
( R is alliance iff the InternalRel of R is_alliance_in the carrier of R );