let R be non empty RelStr ; :: thesis: ( R is positive_alliance implies R is serial )

assume AA: R is positive_alliance ; :: thesis: R is serial

set X = the carrier of R;

set I = the InternalRel of R;

b2: the InternalRel of R is_positive_alliance_in the carrier of R by AA;

for x being object st x in the carrier of R holds

ex y being object st

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

assume AA: R is positive_alliance ; :: thesis: R is serial

set X = the carrier of R;

set I = the InternalRel of R;

b2: the InternalRel of R is_positive_alliance_in the carrier of R by AA;

for x being object st x in the carrier of R holds

ex y being object st

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

proof

hence
R is serial
by ROUGHS_2:def 3, ROUGHS_2:def 1; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier of R implies ex y being object st

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

assume B0: x in the carrier of R ; :: thesis: ex y being object st

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

ex y being object st

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

( y in the carrier of R & [x,y] in the InternalRel of R ) ; :: thesis: verum

end;( y in the carrier of R & [x,y] in the InternalRel of R ) )

assume B0: x in the carrier of R ; :: thesis: ex y being object st

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

ex y being object st

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

proof
end;

hence
ex y being object st per cases
( [x,x] in the InternalRel of R or not [x,x] in the InternalRel of R )
;

end;

suppose
[x,x] in the InternalRel of R
; :: thesis: ex y being object st

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

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

hence
ex y being object st

( y in the carrier of R & [x,y] in the InternalRel of R ) by B0; :: thesis: verum

end;( y in the carrier of R & [x,y] in the InternalRel of R ) by B0; :: thesis: verum

suppose
not [x,x] in the InternalRel of R
; :: thesis: ex y being object st

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

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

then consider z being object such that

B3: ( z in the carrier of R & [x,z] in the InternalRel of R & not [z,x] in the InternalRel of R ) by B0, b2;

thus ex y being object st

( y in the carrier of R & [x,y] in the InternalRel of R ) by B3; :: thesis: verum

end;B3: ( z in the carrier of R & [x,z] in the InternalRel of R & not [z,x] in the InternalRel of R ) by B0, b2;

thus ex y being object st

( y in the carrier of R & [x,y] in the InternalRel of R ) by B3; :: thesis: verum

( y in the carrier of R & [x,y] in the InternalRel of R ) ; :: thesis: verum