let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( not Y c= field () or Y = {} or ex b1 being object st
( b1 in Y & () -Seg b1 misses Y ) )

assume that
A3: Y c= field () and
A4: Y <> {} ; :: thesis: ex b1 being object st
( b1 in Y & () -Seg b1 misses Y )

defpred S1[ set ] means A in Y;
set x = the Element of Y;
A5: field () = 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 S1[B] ;
consider B being Ordinal such that
A7: ( S1[B] & ( for C being Ordinal st S1[C] holds
B c= C ) ) from reconsider x = B as set ;
take x ; :: thesis: ( x in Y & () -Seg x misses Y )
thus x in Y by A7; :: thesis: () -Seg x misses Y
set y = the Element of (() -Seg x) /\ Y;
assume A8: ((RelIncl A) -Seg x) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then A9: the Element of (() -Seg x) /\ Y in Y by XBOOLE_0:def 4;
then reconsider C = the Element of (() -Seg x) /\ Y as Ordinal by A3, A5;
A10: the Element of (() -Seg x) /\ Y in () -Seg x by ;
then [ the Element of (() -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 (() -Seg x) /\ Y <> x by ;
B c= C by A7, A9;
hence contradiction by A12, A11; :: thesis: verum