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

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