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