let L be RelStr ; 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 ; 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 \~); ( 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 ( 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 \~)
;
( 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;
for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of Llet y be
Element of
L;
( y in N & [y,x] in the InternalRel of L implies [x,y] in the InternalRel of L )assume A2:
y in N
;
( [y,x] in the InternalRel of L implies [x,y] in the InternalRel of L )assume A3:
[y,x] in the
InternalRel of
L
;
[x,y] in the InternalRel of Lhence
[x,y] in the
InternalRel of
L
;
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
; x is_minimal_wrt N, the InternalRel of (L \~)
now 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 \~) )
;
contradictionthen 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;
verum end;
hence
x is_minimal_wrt N, the InternalRel of (L \~)
by A4, WAYBEL_4:def 25; verum