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 IR9 = 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 25; :: 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 :: thesis: [x,y] in the InternalRel of L
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;
end;
end;
hence [x,y] in the InternalRel of L ; :: thesis: verum
end;
assume that
A4: x in N and
A5: 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 :: thesis: for y being set holds
( not y in N or not y <> x or not [y,x] in the InternalRel of (L \~) )
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
A6: y in N and
y <> x and
A7: [y,x] in the InternalRel of (L \~) ;
reconsider y9 = y as Element of L by A7, ZFMISC_1:87;
A8: not [y,x] in the InternalRel of L ~ by A7, XBOOLE_0:def 5;
( [y9,x] in the InternalRel of L implies [x,y9] in the InternalRel of L ) by A5, A6;
hence contradiction by A7, A8, RELAT_1:def 7; :: thesis: verum
end;
hence x is_minimal_wrt N, the InternalRel of (L \~) by A4, WAYBEL_4:def 25; :: thesis: verum