let S be non empty RelStr ; :: thesis: ( S is tournament iff SymmetricHull S = nabla the carrier of S )
thus ( S is tournament implies SymmetricHull S = nabla the carrier of S ) :: thesis: ( SymmetricHull S = nabla the carrier of S implies S is tournament )

proof

assume S is tournament ; :: thesis: SymmetricHull S = nabla the carrier of S
then Aa1: for a, b being Element of S holds
( a <= b or b <= a ) ;
for a, b being object st [a,b] in SymmetricHull S holds
[a,b] in nabla the carrier of S

proof

let a, b be object ; :: thesis: ( [a,b] in SymmetricHull S implies [a,b] in nabla the carrier of S )
assume [a,b] in SymmetricHull S ; :: thesis: [a,b] in nabla the carrier of S
then [a,b] in [: the carrier of S, the carrier of S:] ;
hence [a,b] in nabla the carrier of S by EQREL_1:def 1; :: thesis: verum

end;

then A1: SymmetricHull S c= nabla the carrier of S by RELAT_1:def 3;
for a, b being object st [a,b] in nabla the carrier of S holds
[a,b] in SymmetricHull S

proof

let a, b be object ; :: thesis: ( [a,b] in nabla the carrier of S implies [a,b] in SymmetricHull S )
assume [a,b] in nabla the carrier of S ; :: thesis: [a,b] in SymmetricHull S
then Z9: [a,b] in [: the carrier of S, the carrier of S:] ;
then reconsider aa = a as Element of S by ZFMISC_1:87;
reconsider bb = b as Element of S by Z9, ZFMISC_1:87;
( aa <= bb or bb <= aa ) by Aa1;
hence [a,b] in SymmetricHull S by SymHull; :: thesis: verum

end;

then nabla the carrier of S c= SymmetricHull S by RELAT_1:def 3;
hence SymmetricHull S = nabla the carrier of S by A1, XBOOLE_0:def 10; :: thesis: verum

end;

assume W0: SymmetricHull S = nabla the carrier of S ; :: thesis: S is tournament
for x, y being Element of S holds
( x <= y or y <= x )

proof

let x, y be Element of S; :: thesis: ( x <= y or y <= x )
[x,y] in [: the carrier of S, the carrier of S:] by ZFMISC_1:87;
then [x,y] in nabla the carrier of S by EQREL_1:def 1;
hence ( x <= y or y <= x ) by W0, SymHull; :: thesis: verum

end;

hence S is tournament ; :: thesis: verum