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 B1, WELLFND1:def 2;
then consider a0 being set such that
A1: a0 in C and
A2: the InternalRel of R -Seg a0 misses C by B2, WELLORD1:def 3;
reconsider a0 = a0 as Element of R by B2, A1;
take a0 ; :: thesis: ( a0 in C & a0 is_minimal_wrt C, the InternalRel of R )
thus a0 in C by A1; :: thesis: a0 is_minimal_wrt C, the InternalRel of R
thus a0 is_minimal_wrt C, the InternalRel of R by A1, A2, DICKSON:6; :: thesis: verum