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