theorem Th14: :: SYSREL:14
for X, Y being set holds
( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )