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;
set x = the Element of Y;
A3: field (RelIncl A) = A by Def1;
then the Element of Y in A by A1, A2, TARSKI:def 3;
then reconsider x = the Element of Y 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
set y = the Element of ((RelIncl A) -Seg x) /\ Y;
assume A6: ((RelIncl A) -Seg x) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then A7: the Element of ((RelIncl A) -Seg x) /\ Y in Y by XBOOLE_0:def 4;
then reconsider C = the Element of ((RelIncl A) -Seg x) /\ Y as Ordinal by A1, A3;
A8: the Element of ((RelIncl A) -Seg x) /\ Y in (RelIncl A) -Seg x by A6, XBOOLE_0:def 4;
then [ the Element of ((RelIncl A) -Seg x) /\ Y,x] in RelIncl A by WELLORD1:1;
then A9: C c= B by A1, A3, A5, A7, Def1;
A10: the Element of ((RelIncl A) -Seg x) /\ Y <> x by A8, WELLORD1:1;
B c= C by A5, A7;
hence contradiction by A10, A9, XBOOLE_0:def 10; :: thesis: verum