let L be RelStr ; :: thesis: for N being set
for x being Element of (L \~ ) holds
( x is_minimal_wrt N,the InternalRel of (L \~ ) iff ( x in N & ( for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L ) ) )
let N be set ; :: thesis: for x being Element of (L \~ ) holds
( x is_minimal_wrt N,the InternalRel of (L \~ ) iff ( x in N & ( for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L ) ) )
let x be Element of (L \~ ); :: thesis: ( x is_minimal_wrt N,the InternalRel of (L \~ ) iff ( x in N & ( for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L ) ) )
set IR = the InternalRel of L;
set IR' = the InternalRel of (L \~ );

hereby :: thesis: ( x in N & ( for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L ) implies x is_minimal_wrt N,the InternalRel of (L \~ ) )

assume A1: x is_minimal_wrt N,the InternalRel of (L \~ ) ; :: thesis: ( x in N & ( for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L ) )
hence x in N by WAYBEL_4:def 26; :: thesis: for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L
let y be Element of L; :: thesis: ( y in N & [y,x] in the InternalRel of L implies [x,y] in the InternalRel of L )
assume A2: y in N ; :: thesis: ( [y,x] in the InternalRel of L implies [x,y] in the InternalRel of L )
assume A3: [y,x] in the InternalRel of L ; :: thesis: [x,y] in the InternalRel of L

now

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: [x,y] in the InternalRel of L

hence [x,y] in the InternalRel of L by A3; :: thesis: verum

end;

suppose x <> y ; :: thesis: [x,y] in the InternalRel of L

then not [y,x] in the InternalRel of (L \~ ) by A1, A2, WAYBEL_4:def 26;
then [y,x] in the InternalRel of L ~ by A3, XBOOLE_0:def 5;
hence [x,y] in the InternalRel of L by RELAT_1:def 7; :: thesis: verum

end;

end;

end;

hence [x,y] in the InternalRel of L ; :: thesis: verum

end;

assume A4: ( x in N & ( for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L ) ) ; :: thesis: x is_minimal_wrt N,the InternalRel of (L \~ )

now

thus x in N by A4; :: thesis: for y being set holds
( not y in N or not y <> x or not [y,x] in the InternalRel of (L \~ ) )

now

assume ex y being set st
( y in N & y <> x & [y,x] in the InternalRel of (L \~ ) ) ; :: thesis: contradiction
then consider y being set such that
A5: y in N and
y <> x and
A6: [y,x] in the InternalRel of (L \~ ) ;
reconsider y' = y as Element of L by A6, ZFMISC_1:106;
A7: ( [y,x] in the InternalRel of L & not [y,x] in the InternalRel of L ~ ) by A6, XBOOLE_0:def 5;
( [y',x] in the InternalRel of L implies [x,y'] in the InternalRel of L ) by A4, A5;
hence contradiction by A7, RELAT_1:def 7; :: thesis: verum

end;

hence for y being set holds
( not y in N or not y <> x or not [y,x] in the InternalRel of (L \~ ) ) ; :: thesis: verum

end;

hence x is_minimal_wrt N,the InternalRel of (L \~ ) by WAYBEL_4:def 26; :: thesis: verum