let A, B be Ordinal; :: thesis: ( A c= B implies Positives A c= Positives B )
assume A1: A c= B ; :: thesis: Positives A c= Positives B
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in Positives A or [x,y] in Positives B )
assume A2: [x,y] in Positives A ; :: thesis: [x,y] in Positives B
then reconsider xy = [x,y] as Surreal ;
( xy in Day A & Day A c= Day B & 0_No < xy ) by A1, A2, Def10, SURREAL0:35;
hence [x,y] in Positives B by Def10; :: thesis: verum