let X, Y be set ; :: thesis: ( X is epsilon-transitive & Y is epsilon-transitive implies X /\ Y is epsilon-transitive )
assume that
A1: for Z being set st Z in X holds
Z c= X and
A2: for Z being set st Z in Y holds
Z c= Y ; :: according to ORDINAL1:def 2 :: thesis: X /\ Y is epsilon-transitive
let Z be set ; :: according to ORDINAL1:def 2 :: thesis: ( not Z in X /\ Y or Z c= X /\ Y )
assume A3: Z in X /\ Y ; :: thesis: Z c= X /\ Y
then A4: Z in X by XBOOLE_0:def 4;
A5: Z in Y by A3, XBOOLE_0:def 4;
A6: Z c= X by A1, A4;
Z c= Y by A2, A5;
hence Z c= X /\ Y by A6, XBOOLE_1:19; :: thesis: verum