let A, B, C, D, E, X be set ; :: thesis: ( ( X c= A or X c= B or X c= C or X c= D or X c= E ) implies X c= (((A \/ B) \/ C) \/ D) \/ E )
assume A1: ( X c= A or X c= B or X c= C or X c= D or X c= E ) ; :: thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
per cases ( X c= A or X c= B or X c= C or X c= D or X c= E ) by A1;
suppose X c= A ; :: thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
then X c= A \/ B by XBOOLE_1:10;
then X c= (A \/ B) \/ C by XBOOLE_1:10;
then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10;
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; :: thesis: verum
end;
suppose X c= B ; :: thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
then X c= A \/ B by XBOOLE_1:10;
then X c= (A \/ B) \/ C by XBOOLE_1:10;
then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10;
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; :: thesis: verum
end;
suppose X c= C ; :: thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
then X c= (A \/ B) \/ C by XBOOLE_1:10;
then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10;
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; :: thesis: verum
end;
suppose X c= D ; :: thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10;
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; :: thesis: verum
end;
suppose X c= E ; :: thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; :: thesis: verum
end;
end;