let R be non empty RelStr ; ( R is discrete implies R is negative_alliance )
assume AA:
R is discrete
; R is negative_alliance
set X = the carrier of R;
set I = the InternalRel of R;
let x, y be object ; ROUGHS_3:def 6,ROUGHS_3:def 9 ( 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 )
; ( 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 )
; 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; verum