let R be non empty RelStr ; :: thesis: ( R is positive_alliance & R is negative_alliance implies R is alliance )
set I = the InternalRel of R;
set X = the carrier of R;
assume ( R is positive_alliance & R is negative_alliance ) ; :: thesis: R is alliance
then the InternalRel of R is_alliance_in the carrier of R ;
hence R is alliance ; :: thesis: verum