let R be non empty RelStr ; :: thesis: ( R is discrete implies R is negative_alliance )

assume AA: R is discrete ; :: thesis: R is negative_alliance

set X = the carrier of R;

set I = the InternalRel of R;

let x, y be object ; :: according to ROUGHS_3:def 6,ROUGHS_3:def 9 :: thesis: ( x in the carrier of R & y in the carrier of R & ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) implies not [x,y] in the InternalRel of R )

assume ( x in the carrier of R & y in the carrier of R ) ; :: thesis: ( for z being object holds

( not z in the carrier of R or not [x,z] in the InternalRel of R or [z,y] in the InternalRel of R ) or not [x,y] in the InternalRel of R )

then reconsider x1 = x as Element of R ;

given z being object such that E1: ( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) ; :: thesis: not [x,y] in the InternalRel of R

reconsider z1 = z as Element of R by E1;

x1 <= z1 by E1, ORDERS_2:def 5;

hence not [x,y] in the InternalRel of R by E1, AA, ORDERS_3:1; :: thesis: verum

assume AA: R is discrete ; :: thesis: R is negative_alliance

set X = the carrier of R;

set I = the InternalRel of R;

let x, y be object ; :: according to ROUGHS_3:def 6,ROUGHS_3:def 9 :: thesis: ( x in the carrier of R & y in the carrier of R & ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) implies not [x,y] in the InternalRel of R )

assume ( x in the carrier of R & y in the carrier of R ) ; :: thesis: ( for z being object holds

( not z in the carrier of R or not [x,z] in the InternalRel of R or [z,y] in the InternalRel of R ) or not [x,y] in the InternalRel of R )

then reconsider x1 = x as Element of R ;

given z being object such that E1: ( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) ; :: thesis: not [x,y] in the InternalRel of R

reconsider z1 = z as Element of R by E1;

x1 <= z1 by E1, ORDERS_2:def 5;

hence not [x,y] in the InternalRel of R by E1, AA, ORDERS_3:1; :: thesis: verum