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

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

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 ; :: according to TARSKI:def 3 :: thesis: ( not a in (RelIncl B) -Seg A or a in A )
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;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

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