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

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