let X, Y be set ; :: thesis: (succRel X) \/ (succRel Y) c= succRel (X \/ Y)
( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
then ( succRel X c= succRel (X \/ Y) & succRel Y c= succRel (X \/ Y) ) by Th1;
hence (succRel X) \/ (succRel Y) c= succRel (X \/ Y) by XBOOLE_1:8; :: thesis: verum