let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( not Y c= field (RelIncl A) or Y = {} or ex b_{1} being object st

( b_{1} in Y & (RelIncl A) -Seg b_{1} misses Y ) )

assume that

A3: Y c= field (RelIncl A) and

A4: Y <> {} ; :: thesis: ex b_{1} being object st

( b_{1} in Y & (RelIncl A) -Seg b_{1} misses Y )

defpred S_{1}[ 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_{1}[B]
;

consider B being Ordinal such that

A7: ( S_{1}[B] & ( for C being Ordinal st S_{1}[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

( b

assume that

A3: Y c= field (RelIncl A) and

A4: Y <> {} ; :: thesis: ex b

( b

defpred S

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

consider B being Ordinal such that

A7: ( S

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