set IR = the InternalRel of R;

set CR = the carrier of R;

the InternalRel of R is_well_founded_in the carrier of R by A1;

then consider a0 being object such that

A3: a0 in C and

A4: the InternalRel of R -Seg a0 misses C by A2, WELLORD1:def 3;

reconsider a0 = a0 as Element of R by A2, A3;

take a0 ; :: thesis: ( a0 in C & a0 is_minimal_wrt C, the InternalRel of R )

thus a0 in C by A3; :: thesis: a0 is_minimal_wrt C, the InternalRel of R

thus a0 is_minimal_wrt C, the InternalRel of R by A3, A4, DICKSON:6; :: thesis: verum

set CR = the carrier of R;

the InternalRel of R is_well_founded_in the carrier of R by A1;

then consider a0 being object such that

A3: a0 in C and

A4: the InternalRel of R -Seg a0 misses C by A2, WELLORD1:def 3;

reconsider a0 = a0 as Element of R by A2, A3;

take a0 ; :: thesis: ( a0 in C & a0 is_minimal_wrt C, the InternalRel of R )

thus a0 in C by A3; :: thesis: a0 is_minimal_wrt C, the InternalRel of R

thus a0 is_minimal_wrt C, the InternalRel of R by A3, A4, DICKSON:6; :: thesis: verum