let R be non empty RelStr ; for N being Subset of R
for x being set st R is quasi_ordered & x in min-classes N holds
for y being Element of (R \~) st y in x holds
y is_minimal_wrt N, the InternalRel of (R \~)
let N be Subset of R; for x being set st R is quasi_ordered & x in min-classes N holds
for y being Element of (R \~) st y in x holds
y is_minimal_wrt N, the InternalRel of (R \~)
let x be set ; ( R is quasi_ordered & x in min-classes N implies for y being Element of (R \~) st y in x holds
y is_minimal_wrt N, the InternalRel of (R \~) )
assume that
A1:
R is quasi_ordered
and
A2:
x in min-classes N
; for y being Element of (R \~) st y in x holds
y is_minimal_wrt N, the InternalRel of (R \~)
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);
let c be Element of (R \~); ( c in x implies c is_minimal_wrt N, the InternalRel of (R \~) )
assume A3:
c in x
; c is_minimal_wrt N, the InternalRel of (R \~)
consider b being Element of (R \~) such that
A4:
b is_minimal_wrt N, the InternalRel of (R \~)
and
A5:
x = (Class ((EqRel R),b)) /\ N
by A2, Def8;
c in Class ((EqRel R),b)
by A3, A5, XBOOLE_0:def 4;
then
[c,b] in EqRel R
by EQREL_1:19;
then
[c,b] in the InternalRel of R /\ ( the InternalRel of R ~)
by A1, Def4;
then A6:
[c,b] in the InternalRel of R
by XBOOLE_0:def 4;
A7:
now for d being set holds
( not d in N or not d <> c or not [d,c] in the InternalRel of (R \~) )assume
ex
d being
set st
(
d in N &
d <> c &
[d,c] in the
InternalRel of
(R \~) )
;
contradictionthen consider d being
set such that A8:
d in N
and
d <> c
and A9:
[d,c] in the
InternalRel of
(R \~)
;
A10:
not
[d,c] in the
InternalRel of
R ~
by A9, XBOOLE_0:def 5;
R is
transitive
by A1;
then A11:
the
InternalRel of
R is_transitive_in the
carrier of
R
;
then A12:
[d,b] in the
InternalRel of
R
by A6, A8, A9;
then A13:
[d,b] in the
InternalRel of
(R \~)
by A12, XBOOLE_0:def 5;
b <> d
by A6, A10, RELAT_1:def 7;
hence
contradiction
by A4, A8, A13, WAYBEL_4:def 25;
verum end;
c in N
by A3, A5, XBOOLE_0:def 4;
hence
c is_minimal_wrt N, the InternalRel of (R \~)
by A7, WAYBEL_4:def 25; verum