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 Z in X \/ Y ; :: thesis: Z c= X \/ Y
then ( Z in X or Z in Y ) by XBOOLE_0:def 3;
then A3: ( Z c= X or Z c= Y ) by A1, A2;
( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
hence Z c= X \/ Y by A3; :: thesis: verum