let S be surreal-membered set ; :: thesis: field the InternalRel of (RevSurrStr S) = S
set I = the InternalRel of (RevSurrStr S);
set R = RevSurrStr S;
set I = the InternalRel of (RevSurrStr S);
the carrier of (RevSurrStr S) = S by Def10;
then A1: field the InternalRel of (RevSurrStr S) c= S \/ S by RELSET_1:8;
S c= field the InternalRel of (RevSurrStr S)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in S or a in field the InternalRel of (RevSurrStr S) )
assume A2: a in S ; :: thesis: a in field the InternalRel of (RevSurrStr S)
then reconsider x = a as Surreal by SURREAL0:def 16;
[x,x] in the InternalRel of (RevSurrStr S) by A2, Def10;
hence a in field the InternalRel of (RevSurrStr S) by RELAT_1:15; :: thesis: verum

end;

hence field the InternalRel of (RevSurrStr S) = S by A1; :: thesis: verum