set R = the InternalRel of T;
thus
( T is Noetherian implies for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) ) )
( ( for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) ) ) implies T is Noetherian )
assume A9:
for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) )
; T is Noetherian
let Y be set ; REWRITE1:def 16,ABCMIZ_0:def 1 ( not Y c= field the InternalRel of T or Y = {} or ex b1 being object st
( b1 in Y & ( for b2 being object holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of T ) ) ) )
assume that
A10:
Y c= field the InternalRel of T
and
A11:
Y <> {}
; ex b1 being object st
( b1 in Y & ( for b2 being object holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of T ) ) )
field the InternalRel of T c= the carrier of T \/ the carrier of T
by RELSET_1:8;
then reconsider A = Y as non empty Subset of T by A10, A11, XBOOLE_1:1;
consider a being Element of T such that
A12:
a in A
and
A13:
for b being Element of T st b in A holds
not a < b
by A9;
take
a
; ( a in Y & ( for b1 being object holds
( not b1 in Y or a = b1 or not [a,b1] in the InternalRel of T ) ) )
thus
a in Y
by A12; for b1 being object holds
( not b1 in Y or a = b1 or not [a,b1] in the InternalRel of T )
let b be object ; ( not b in Y or a = b or not [a,b] in the InternalRel of T )
assume that
A14:
b in Y
and
A15:
a <> b
; not [a,b] in the InternalRel of T
b in A
by A14;
then reconsider b = b as Element of T ;
not a < b
by A13, A14;
then
not a <= b
by A15, ORDERS_2:def 6;
hence
not [a,b] in the InternalRel of T
by ORDERS_2:def 5; verum