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 )

proof

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 )

proof

per cases ( [x,x] in the InternalRel of R or not [x,x] in the InternalRel of R ) ;

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 )

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

end;

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 )

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;

end;

end;

hence ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R ) ; :: thesis: verum

end;

hence R is serial by ROUGHS_2:def 3, ROUGHS_2:def 1; :: thesis: verum