let A, B be Ordinal; :: thesis: ( A in B implies A = (RelIncl B) -Seg A )
assume A1: A in B ; :: thesis: A = (RelIncl B) -Seg A
thus for a being object st a in A holds
a in (RelIncl B) -Seg A :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (RelIncl B) -Seg A c= A

proof

let a be object ; :: thesis: ( a in A implies a in (RelIncl B) -Seg A )
assume A2: a in A ; :: thesis: a in (RelIncl B) -Seg A
then reconsider C = a as Ordinal ;
reconsider a = a as set by TARSKI:1;
not a in a ;
then A3: a <> A by A2;
A4: A c= B by A1, ORDINAL1:def 2;
C c= A by A2, ORDINAL1:def 2;
then [C,A] in RelIncl B by A1, A2, A4, Def1;
hence a in (RelIncl B) -Seg A by A3, WELLORD1:1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (RelIncl B) -Seg A or a in A )
assume A5: a in (RelIncl B) -Seg A ; :: thesis: a in A
then A6: a <> A by WELLORD1:1;
A7: [a,A] in RelIncl B by A5, WELLORD1:1;
then A8: a in field (RelIncl B) by RELAT_1:15;
A9: field (RelIncl B) = B by Def1;
then reconsider C = a as Ordinal by A8;
C c= A by A1, A7, A8, A9, Def1;
then C c< A by A6;
hence a in A by ORDINAL1:11; :: thesis: verum