let R be non empty RelStr ; ( R is reflexive implies R is positive_alliance )
assume AA:
R is reflexive
; 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
let x,
y be
object ;
ROUGHS_3:def 5 ( 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 )
;
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;
verum
end;
hence
R is positive_alliance
; verum