set R = the non empty reflexive discrete RelStr ;
the non empty reflexive discrete RelStr is positive_alliance ;
hence ex b₁ being non empty RelStr st
( b₁ is positive_alliance & b₁ is negative_alliance ) ; :: thesis: verum