let R be RelStr ; for N being Subset of R
for x being Element of (R \~) st R is quasi_ordered & x in N & ( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x) holds
x is_minimal_wrt N, the InternalRel of (R \~)
let N be Subset of R; for x being Element of (R \~) st R is quasi_ordered & x in N & ( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x) holds
x is_minimal_wrt N, the InternalRel of (R \~)
let x be Element of (R \~); ( R is quasi_ordered & x in N & ( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x) implies x is_minimal_wrt N, the InternalRel of (R \~) )
assume that
A1:
R is quasi_ordered
and
A2:
x in N
and
A3:
( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x)
; x is_minimal_wrt N, the InternalRel of (R \~)
set IR = the InternalRel of R;
set IR9 = the InternalRel of (R \~);
now for y being set holds
( not y in N or not y <> x or not [y,x] in the InternalRel of (R \~) )assume
ex
y being
set st
(
y in N &
y <> x &
[y,x] in the
InternalRel of
(R \~) )
;
contradictionthen consider y being
set such that A4:
y in N
and A5:
y <> x
and A6:
[y,x] in the
InternalRel of
(R \~)
;
A7:
not
[y,x] in the
InternalRel of
R ~
by A6, XBOOLE_0:def 5;
y in the
InternalRel of
R -Seg x
by A5, A6, WELLORD1:1;
then
y in ( the InternalRel of R -Seg x) /\ N
by A4, XBOOLE_0:def 4;
then
[y,x] in EqRel R
by A3, EQREL_1:19;
then
[y,x] in the
InternalRel of
R /\ ( the InternalRel of R ~)
by A1, Def4;
hence
contradiction
by A7, XBOOLE_0:def 4;
verum end;
hence
x is_minimal_wrt N, the InternalRel of (R \~)
by A2, WAYBEL_4:def 25; verum