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

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