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 ; RELAT_2:def 6,RELAT_2:def 14 ( 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 )
; ( [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 )
; verum