let S, T be surreal-membered set ; :: thesis: ( S c= T implies Unique_No S c= Unique_No T )
assume A1: S c= T ; :: thesis: Unique_No S c= Unique_No T
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Unique_No S or x in Unique_No T )
assume A2: x in Unique_No S ; :: thesis: x in Unique_No T
then reconsider s = x as uSurreal by SURREALO:def 12;
ex y being Surreal st
( y in S & s = Unique_No y ) by A2, Def8;
hence x in Unique_No T by A1, Def8; :: thesis: verum