set R = R1 \, R2;
A1: ( field (R1 \, R2) = X & field R2 = X ) by ORDERS_1:12;
then A2: R2 is_connected_in X by RELAT_2:def 14;
let x, y be object ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: ( not x in field (R1 \, R2) or not y in field (R1 \, R2) or x = y or [x,y] in R1 \, R2 or [y,x] in R1 \, R2 )
reconsider xx = x, yy = y as set by TARSKI:1;
assume ( x in field (R1 \, R2) & y in field (R1 \, R2) & x <> y ) ; :: thesis: ( [x,y] in R1 \, R2 or [y,x] in R1 \, R2 )
then ( [x,y] in R2 or [y,x] in R2 ) by A1, A2;
then ( xx,yy in R1 or ( yy,xx nin R1 & xx,yy in R2 ) or yy,xx in R1 or ( xx,yy nin R1 & yy,xx in R2 ) ) ;
then ( xx,yy in R1 \, R2 or yy,xx in R1 \, R2 ) by Th9;
hence ( [x,y] in R1 \, R2 or [y,x] in R1 \, R2 ) ; :: thesis: verum