let a be set ; :: thesis: for R being Relation st R is well-ordering holds
field (R |_2 (R -Seg a)) = R -Seg a
let R be Relation; :: thesis: ( R is well-ordering implies field (R |_2 (R -Seg a)) = R -Seg a )
R -Seg a c= field R by Th13;
hence ( R is well-ordering implies field (R |_2 (R -Seg a)) = R -Seg a ) by Th39; :: thesis: verum