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