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 set st
( a in Y & ( for b being set 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 ) )
consider a being Element of A;
reconsider a = 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 ( b in A & a < b ) ; :: thesis: contradiction
then a <= b by ORDERS_2:def 10;
then [a,b] in the InternalRel of T by ORDERS_2:def 9;
then a in field the InternalRel of T by RELAT_1:30;
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) c= field the InternalRel of T & A /\ (field the InternalRel of T) <> {} ) by XBOOLE_0:def 7, XBOOLE_1:17;
then consider x being set such that
A3: x in A /\ (field the InternalRel of T) and
A4: for y being set st y in A /\ (field the InternalRel of T) & x <> y holds
not [x,y] in the InternalRel of T by A1;
reconsider x = x as Element of T by A3;
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 A3, 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 A5: ( b in A & x < b ) ; :: thesis: contradiction
then ( x <= b & x <> b ) by ORDERS_2:def 10;
then A6: [x,b] in the InternalRel of T by ORDERS_2:def 9;
then b in field the InternalRel of T by RELAT_1:30;
then b in A /\ (field the InternalRel of T) by A5, XBOOLE_0:def 4;
hence contradiction by A4, A5, A6; :: thesis: verum

end;

end;

end;

assume A7: 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 set st
( b₁ in Y & ( for b₂ being set holds
( not b₂ in Y or b₁ = b₂ or not [b₁,b₂] in the InternalRel of T ) ) ) )
assume A8: ( Y c= field the InternalRel of T & Y <> {} ) ; :: thesis: ex b₁ being set st
( b₁ in Y & ( for b₂ being set 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:19;
then reconsider A = Y as non empty Subset of T by A8, XBOOLE_1:1;
consider a being Element of T such that
A9: a in A and
A10: for b being Element of T st b in A holds
not a < b by A7;
take a ; :: thesis: ( a in Y & ( for b₁ being set holds
( not b₁ in Y or a = b₁ or not [a,b₁] in the InternalRel of T ) ) )
thus a in Y by A9; :: thesis: for b₁ being set holds
( not b₁ in Y or a = b₁ or not [a,b₁] in the InternalRel of T )
let b be set ; :: thesis: ( not b in Y or a = b or not [a,b] in the InternalRel of T )
assume A11: ( b in Y & a <> b ) ; :: thesis: not [a,b] in the InternalRel of T
then b in A ;
then reconsider b = b as Element of T ;
not a < b by A10, A11;
then not a <= b by A11, ORDERS_2:def 10;
hence not [a,b] in the InternalRel of T by ORDERS_2:def 9; :: thesis: verum