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

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