let X, Y be set ; :: thesis: succRel (X /\ Y) = (succRel X) /\ (succRel Y)

now :: thesis: for z being object holds
( ( z in succRel (X /\ Y) implies ( z in succRel X & z in succRel Y ) ) & ( z in succRel X & z in succRel Y implies z in succRel (X /\ Y) ) )

let z be object ; :: thesis: ( ( z in succRel (X /\ Y) implies ( z in succRel X & z in succRel Y ) ) & ( z in succRel X & z in succRel Y implies z in succRel (X /\ Y) ) )

hereby :: thesis: ( z in succRel X & z in succRel Y implies z in succRel (X /\ Y) )

assume A1: z in succRel (X /\ Y) ; :: thesis: ( z in succRel X & z in succRel Y )
then consider x, y being object such that
A2: z = [x,y] by RELAT_1:def 1;
reconsider a = x, b = y as set by TARSKI:1;
[a,b] in succRel (X /\ Y) by A1, A2;
then ( a in X /\ Y & b in X /\ Y & b = succ a ) by Def1;
then ( a in X & b in X & a in Y & b in Y & b = succ a ) by XBOOLE_0:def 4;
hence ( z in succRel X & z in succRel Y ) by A2, Def1; :: thesis: verum

end;

assume A3: ( z in succRel X & z in succRel Y ) ; :: thesis: z in succRel (X /\ Y)
then consider x, y being object such that
A4: z = [x,y] by RELAT_1:def 1;
reconsider a = x, b = y as set by TARSKI:1;
( [a,b] in succRel X & [a,b] in succRel Y ) by A3, A4;
then ( a in X & b in X & a in Y & b in Y & b = succ a ) by Def1;
then ( a in X /\ Y & b in X /\ Y & b = succ a ) by XBOOLE_0:def 4;
hence z in succRel (X /\ Y) by A4, Def1; :: thesis: verum

end;

hence succRel (X /\ Y) = (succRel X) /\ (succRel Y) by XBOOLE_0:def 4; :: thesis: verum