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; :: thesis: verum