let R be Order of X; :: thesis: R is well_founded
let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( not Y c= field R or Y = {} or ex b1 being object st
( b1 in Y & R -Seg b1 misses Y ) )
assume A1: ( Y c= field R & Y <> {} ) ; :: thesis: ex b1 being object st
( b1 in Y & R -Seg b1 misses Y )
defpred S1[ set ] means ( X <> {} implies ex a being set st
( a in X & R -Seg a misses X ) );
A2: Y is finite by A1;
A3: S1[ {} ] ;
A4: for x, B being set st x in Y & B c= Y & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] )
assume that
A5: ( x in Y & B c= Y & S1[B] ) and
B \/ {x} <> {} ; :: thesis: ex a being set st
( a in B \/ {x} & R -Seg a misses B \/ {x} )
per cases ( B = {} or B <> {} ) ;
suppose A6: B = {} ; :: thesis: ex a being set st
( a in B \/ {x} & R -Seg a misses B \/ {x} )
take a = x; :: thesis: ( a in B \/ {x} & R -Seg a misses B \/ {x} )
thus a in B \/ {x} by A6, TARSKI:def 1; :: thesis: R -Seg a misses B \/ {x}
x nin R -Seg a by WELLORD1:1;
hence R -Seg a misses B \/ {x} by A6, ZFMISC_1:50; :: thesis: verum
end;
suppose B <> {} ; :: thesis: ex a being set st
( a in B \/ {x} & R -Seg a misses B \/ {x} )
then consider a being set such that
A7: ( a in B & R -Seg a misses B ) by A5;
per cases ( x nin R -Seg a or x in R -Seg a ) ;
suppose x nin R -Seg a ; :: thesis: ex a being set st
( a in B \/ {x} & R -Seg a misses B \/ {x} )
then A8: R -Seg a misses {x} by ZFMISC_1:50;
take a ; :: thesis: ( a in B \/ {x} & R -Seg a misses B \/ {x} )
thus a in B \/ {x} by A7, XBOOLE_0:def 3; :: thesis: R -Seg a misses B \/ {x}
thus R -Seg a misses B \/ {x} by A7, A8, XBOOLE_1:70; :: thesis: verum
end;
suppose x in R -Seg a ; :: thesis: ex a being set st
( a in B \/ {x} & R -Seg a misses B \/ {x} )
then A9: ( x <> a & [x,a] in R ) by WELLORD1:1;
take b = x; :: thesis: ( b in B \/ {x} & R -Seg b misses B \/ {x} )
b in {x} by TARSKI:def 1;
hence b in B \/ {x} by XBOOLE_0:def 3; :: thesis: R -Seg b misses B \/ {x}
assume R -Seg b meets B \/ {x} ; :: thesis: contradiction
then consider c being object such that
A10: ( c in R -Seg b & c in B \/ {x} ) by XBOOLE_0:3;
reconsider cc = c, xx = x, aa = a as set by TARSKI:1;
A11: ( c <> b & [c,b] in R ) by A10, WELLORD1:1;
then ( cc,xx in R & x,a in R ) by A9;
then A12: ( cc,aa in R & c <> a ) by A11, Def2, Def1;
then ( [c,a] in R & ( c in B or c in {x} ) ) by A10, XBOOLE_0:def 3;
then ( c in R -Seg a & c in B ) by A11, A12, TARSKI:def 1, WELLORD1:1;
hence contradiction by A7, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
end;
end;
S1[Y] from FINSET_1:sch 2(A2, A3, A4);
hence ex a being object st
( a in Y & R -Seg a misses Y ) by A1; :: thesis: verum