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

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

set X = the carrier of R;

set I = the InternalRel of R;

the InternalRel of R is_positive_alliance_in the carrier of R

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

set X = the carrier of R;

set I = the InternalRel of R;

the InternalRel of R is_positive_alliance_in the carrier of R

proof

hence
R is positive_alliance
; :: thesis: verum
let x, y be object ; :: according to ROUGHS_3:def 5 :: 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 A1: ( 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 reconsider x1 = x as Element of R ;

[x1,x1] in the InternalRel of R by ORDERS_2:def 5, AA, YELLOW_0:def 1;

hence 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 ) by A1; :: 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 A1: ( 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 reconsider x1 = x as Element of R ;

[x1,x1] in the InternalRel of R by ORDERS_2:def 5, AA, YELLOW_0:def 1;

hence 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 ) by A1; :: thesis: verum