let R be RelStr ; ( R \~ is well_founded & R is antisymmetric implies R is well_founded )
assume that
A1:
R \~ is well_founded
and
A2:
R is antisymmetric
; R is well_founded
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);
A3:
the InternalRel of R is_antisymmetric_in the carrier of R
by A2;
A4:
the InternalRel of (R \~) is_well_founded_in the carrier of R
by A1, WELLFND1:def 2;
now for Y being set st Y c= the carrier of R & Y <> {} holds
ex a being object st
( a in Y & the InternalRel of R -Seg a misses Y )let Y be
set ;
( Y c= the carrier of R & Y <> {} implies ex a being object st
( a in Y & the InternalRel of R -Seg a misses Y ) )assume that A5:
Y c= the
carrier of
R
and A6:
Y <> {}
;
ex a being object st
( a in Y & the InternalRel of R -Seg a misses Y )consider a being
object such that A7:
a in Y
and A8:
the
InternalRel of
(R \~) -Seg a misses Y
by A4, A5, A6, WELLORD1:def 3;
A9:
( the InternalRel of (R \~) -Seg a) /\ Y = {}
by A8, XBOOLE_0:def 7;
take a =
a;
( a in Y & the InternalRel of R -Seg a misses Y )thus
a in Y
by A7;
the InternalRel of R -Seg a misses Ynow not ( the InternalRel of R -Seg a) /\ Y <> {} assume
( the InternalRel of R -Seg a) /\ Y <> {}
;
contradictionthen consider z being
object such that A10:
z in ( the InternalRel of R -Seg a) /\ Y
by XBOOLE_0:def 1;
A11:
z in the
InternalRel of
R -Seg a
by A10, XBOOLE_0:def 4;
A12:
z in Y
by A10, XBOOLE_0:def 4;
A13:
z <> a
by A11, WELLORD1:1;
A14:
[z,a] in the
InternalRel of
R
by A11, WELLORD1:1;
then
not
[a,z] in the
InternalRel of
R
by A3, A5, A7, A12, A13;
then
not
[z,a] in the
InternalRel of
R ~
by RELAT_1:def 7;
then
[z,a] in the
InternalRel of
R \ ( the InternalRel of R ~)
by A14, XBOOLE_0:def 5;
then
z in the
InternalRel of
(R \~) -Seg a
by A13, WELLORD1:1;
hence
contradiction
by A9, A12, XBOOLE_0:def 4;
verum end; hence
the
InternalRel of
R -Seg a misses Y
by XBOOLE_0:def 7;
verum end;
then
the InternalRel of R is_well_founded_in the carrier of R
by WELLORD1:def 3;
hence
R is well_founded
by WELLFND1:def 2; verum