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

assume AA: ( R is transitive & R is serial ) ; :: thesis: R is positive_alliance

set X = the carrier of R;

set I = the InternalRel of R;

for x, y being object st x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R holds

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 )

hence R is positive_alliance ; :: thesis: verum

assume AA: ( R is transitive & R is serial ) ; :: thesis: R is positive_alliance

set X = the carrier of R;

set I = the InternalRel of R;

for x, y being object st x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R holds

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 )

proof

then
the InternalRel of R is_positive_alliance_in the carrier of R
;
let x, y be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R implies 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 ) )

assume A0: ( x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R ) ; :: thesis: 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 )

then consider z being object such that

A1: ( z in the carrier of R & [x,z] in the InternalRel of R ) by ROUGHS_2:def 1, AA, ROUGHS_2:def 3;

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

thus ( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) by A0, A1, AA, ORDERS_2:def 3, RELAT_2:def 8; :: thesis: verum

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

assume A0: ( x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R ) ; :: thesis: 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 )

then consider z being object such that

A1: ( z in the carrier of R & [x,z] in the InternalRel of R ) by ROUGHS_2:def 1, AA, ROUGHS_2:def 3;

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

thus ( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) by A0, A1, AA, ORDERS_2:def 3, RELAT_2:def 8; :: thesis: verum

hence R is positive_alliance ; :: thesis: verum