let R be RelStr ; :: thesis: for x being set holds the InternalRel of R -Seg x c= the carrier of R
let x be set ; :: thesis: the InternalRel of R -Seg x c= the carrier of R
set r = the InternalRel of R;
set c = the carrier of R;
( the InternalRel of R -Seg x c= field the InternalRel of R & field the InternalRel of R c= the carrier of R \/ the carrier of R ) by RELSET_1:8, WELLORD1:9;
hence the InternalRel of R -Seg x c= the carrier of R ; :: thesis: verum