let A, B be Ordinal; :: thesis: ( A c= B implies Triangle A c= Triangle B )
assume A1: A c= B ; :: thesis: Triangle A c= Triangle B
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in Triangle A or [x,y] in Triangle B )
assume A2: [x,y] in Triangle A ; :: thesis: [x,y] in Triangle B
reconsider x = x, y = y as Element of Day A by A2, ZFMISC_1:87;
(born x) (+) (born y) c= A by A2, Def5;
then (born x) (+) (born y) c= B by A1, XBOOLE_1:1;
hence [x,y] in Triangle B by Def5; :: thesis: verum