let S be 1 -element RelStr ; :: thesis: S is Noetherian
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 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 S ) ) ) )
set R = the InternalRel of S;
assume A1: Y c= field the InternalRel of S ; :: thesis: ( 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 S ) ) ) )
assume 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 S ) ) )
then reconsider X = Y as non empty set ;
set a = the Element of X;
take the Element of X ; :: thesis: ( the Element of X in Y & ( for b₁ being object holds
( not b₁ in Y or the Element of X = b₁ or not [ the Element of X,b₁] in the InternalRel of S ) ) )
thus the Element of X in Y ; :: thesis: for b₁ being object holds
( not b₁ in Y or the Element of X = b₁ or not [ the Element of X,b₁] in the InternalRel of S )
A2: the Element of X in field the InternalRel of S by A1;
let b be object ; :: thesis: ( not b in Y or the Element of X = b or not [ the Element of X,b] in the InternalRel of S )
A3: field the InternalRel of S c= the carrier of S \/ the carrier of S by RELSET_1:8;
assume b in Y ; :: thesis: ( the Element of X = b or not [ the Element of X,b] in the InternalRel of S )
then b in field the InternalRel of S by A1;
hence ( the Element of X = b or not [ the Element of X,b] in the InternalRel of S ) by A2, A3, ZFMISC_1:def 10; :: thesis: verum