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 ) ) ) :: thesis: ( ( 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 )

proof

assume A1: for Y being set st Y c= field the InternalRel of T & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in the InternalRel of T ) ) ; :: according to REWRITE1:def 16,ABCMIZ_0:def 1 :: thesis: 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 ) )
let A be non empty Subset of T; :: thesis: ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) )
set a = the Element of A;
reconsider a = the Element of A as Element of T ;
set Y = A /\ (field the InternalRel of T);

per cases ( A misses field the InternalRel of T or A meets field the InternalRel of T ) ;

suppose A2: A misses field the InternalRel of T ; :: thesis: ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) )

take a ; :: thesis: ( a in A & ( for b being Element of T st b in A holds
not a < b ) )
thus a in A ; :: thesis: for b being Element of T st b in A holds
not a < b
let b be Element of T; :: thesis: ( b in A implies not a < b )
assume that
b in A and
A3: a < b ; :: thesis: contradiction
a <= b by A3, ORDERS_2:def 6;
then [a,b] in the InternalRel of T by ORDERS_2:def 5;
then a in field the InternalRel of T by RELAT_1:15;
hence contradiction by A2, XBOOLE_0:3; :: thesis: verum

end;

suppose A meets field the InternalRel of T ; :: thesis: ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) )

then A /\ (field the InternalRel of T) <> {} ;
then consider x being object such that
A4: x in A /\ (field the InternalRel of T) and
A5: for y being object st y in A /\ (field the InternalRel of T) & x <> y holds
not [x,y] in the InternalRel of T by A1, XBOOLE_1:17;
reconsider x = x as Element of T by A4;
take x ; :: thesis: ( x in A & ( for b being Element of T st b in A holds
not x < b ) )
thus x in A by A4, XBOOLE_0:def 4; :: thesis: for b being Element of T st b in A holds
not x < b
let b be Element of T; :: thesis: ( b in A implies not x < b )
assume that
A6: b in A and
A7: x < b ; :: thesis: contradiction
x <= b by A7, ORDERS_2:def 6;
then A8: [x,b] in the InternalRel of T by ORDERS_2:def 5;
then b in field the InternalRel of T by RELAT_1:15;
then b in A /\ (field the InternalRel of T) by A6, XBOOLE_0:def 4;
hence contradiction by A5, A7, A8; :: thesis: verum

end;

end;

end;

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 ) ) ; :: thesis: T is Noetherian
let Y be set ; :: according to REWRITE1:def 16,ABCMIZ_0:def 1 :: thesis: ( not Y c= field the InternalRel of T or Y = {} or ex b₁ being object st
( b₁ in Y & ( for b₂ being object holds
( not b₂ in Y or b₁ = b₂ or not [b₁,b₂] in the InternalRel of T ) ) ) )
assume that
A10: Y c= field the InternalRel of T and
A11: Y <> {} ; :: thesis: ex b₁ being object st
( b₁ in Y & ( for b₂ being object holds
( not b₂ in Y or b₁ = b₂ or not [b₁,b₂] 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 ; :: thesis: ( a in Y & ( for b₁ being object holds
( not b₁ in Y or a = b₁ or not [a,b₁] in the InternalRel of T ) ) )
thus a in Y by A12; :: thesis: for b₁ being object holds
( not b₁ in Y or a = b₁ or not [a,b₁] in the InternalRel of T )
let b be object ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum