set X = dom R;
set i = id (dom R);
set s = Swap ((id (dom R)),x,y);
set h = [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):];
set Y = (succ y) \ x;
set Z1 = [:{x},((succ y) \ x):];
set Z2 = [:((succ y) \ x),{y}:];
set g = id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]);
A1:
((R,x,y) incl) .: z c= rng ((R,x,y) incl)
by RELAT_1:111;
A2:
rng [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] = [:(rng (Swap ((id (dom R)),x,y))),(rng (Swap ((id (dom R)),x,y))):]
by FUNCT_3:67;
rng ((R,x,y) incl) c= (rng [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):]) \/ (rng (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:])))
by FUNCT_4:17;
hence
((R,x,y) incl) .: z is Relation-like
by A1, A2; verum