let A be Ordinal; :: thesis: RelIncl A is well_founded
let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( not Y c= field (RelIncl A) or Y = {} or ex b₁ being set st
( b₁ in Y & (RelIncl A) -Seg b₁ misses Y ) )
assume that
A1: Y c= field (RelIncl A) and
A2: Y <> {} ; :: thesis: ex b₁ being set st
( b₁ in Y & (RelIncl A) -Seg b₁ misses Y )
defpred S₁[ set ] means $1 in Y;
consider x being Element of Y;
A3: field (RelIncl A) = A by Def1;
then x in A by A1, A2, TARSKI:def 3;
then reconsider x = x as Ordinal ;
x in Y by A2;
then A4: ex B being Ordinal st S₁[B] ;
consider B being Ordinal such that
A5: ( S₁[B] & ( for C being Ordinal st S₁[C] holds
B c= C ) ) from ORDINAL1:sch 1(A4);
reconsider x = B as set ;
take x ; :: thesis: ( x in Y & (RelIncl A) -Seg x misses Y )
thus x in Y by A5; :: thesis: (RelIncl A) -Seg x misses Y
consider y being Element of ((RelIncl A) -Seg x) /\ Y;
assume A6: ((RelIncl A) -Seg x) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then A7: y in Y by XBOOLE_0:def 4;
then reconsider C = y as Ordinal by A1, A3;
A8: y in (RelIncl A) -Seg x by A6, XBOOLE_0:def 4;
then [y,x] in RelIncl A by WELLORD1:def 1;
then A9: C c= B by A1, A3, A5, A7, Def1;
A10: y <> x by A8, WELLORD1:def 1;
B c= C by A5, A7;
hence contradiction by A10, A9, XBOOLE_0:def 10; :: thesis: verum