let R be Relation; :: thesis: for A, B being Ordinal st R, RelIncl A are_isomorphic & R, RelIncl B are_isomorphic holds
A = B
let A, B be Ordinal; :: thesis: ( R, RelIncl A are_isomorphic & R, RelIncl B are_isomorphic implies A = B )
assume that
A1: R, RelIncl A are_isomorphic and
A2: R, RelIncl B are_isomorphic ; :: thesis: A = B
RelIncl A,R are_isomorphic by A1, WELLORD1:40;
hence A = B by A2, Th4, WELLORD1:42; :: thesis: verum