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