let S be non empty RelStr ; :: thesis: ( S is trivial implies S is Noetherian )
assume A1:
for x, y being Element of S holds x = y
; :: according to STRUCT_0:def 10 :: thesis: S is Noetherian
set R = the InternalRel of S;
let Y be set ; :: according to REWRITE1:def 16,ABCMIZ_0:def 1 :: thesis: ( not Y c= field the InternalRel of S or Y = {} or ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of S ) ) ) )
assume A2:
Y c= field the InternalRel of S
; :: thesis: ( Y = {} or ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of S ) ) ) )
assume
Y <> {}
; :: thesis: ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of S ) ) )
then reconsider X = Y as non empty set ;
consider a being Element of X;
take
a
; :: thesis: ( a in Y & ( for b1 being set holds
( not b1 in Y or a = b1 or not [a,b1] in the InternalRel of S ) ) )
thus A3:
a in Y
; :: thesis: for b1 being set holds
( not b1 in Y or a = b1 or not [a,b1] in the InternalRel of S )
let b be set ; :: thesis: ( not b in Y or a = b or not [a,b] in the InternalRel of S )
assume
b in Y
; :: thesis: ( a = b or not [a,b] in the InternalRel of S )
then
( a in field the InternalRel of S & b in field the InternalRel of S & field the InternalRel of S c= the carrier of S \/ the carrier of S )
by A2, A3, RELSET_1:19;
hence
( a = b or not [a,b] in the InternalRel of S )
by A1; :: thesis: verum