let A, B, C, D, E, x be set ; :: thesis: ( x in (((A \/ B) \/ C) \/ D) \/ E iff ( x in A or x in B or x in C or x in D or x in E ) )

hereby :: thesis: ( ( x in A or x in B or x in C or x in D or x in E ) implies x in (((A \/ B) \/ C) \/ D) \/ E )

assume x in (((A \/ B) \/ C) \/ D) \/ E ; :: thesis: ( x in A or x in B or x in C or x in D or x in E )
then ( x in ((A \/ B) \/ C) \/ D or x in E ) by XBOOLE_0:def 3;
then ( x in (A \/ B) \/ C or x in D or x in E ) by XBOOLE_0:def 3;
then ( x in A \/ B or x in C or x in D or x in E ) by XBOOLE_0:def 3;
hence ( x in A or x in B or x in C or x in D or x in E ) by XBOOLE_0:def 3; :: thesis: verum

end;

assume A1: ( x in A or x in B or x in C or x in D or x in E ) ; :: thesis: x in (((A \/ B) \/ C) \/ D) \/ E

per cases ( x in A or x in B or x in C or x in D or x in E ) by A1;

suppose x in A ; :: thesis: x in (((A \/ B) \/ C) \/ D) \/ E

then x in A \/ B by XBOOLE_0:def 3;
then x in (A \/ B) \/ C by XBOOLE_0:def 3;
then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def 3;
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in B ; :: thesis: x in (((A \/ B) \/ C) \/ D) \/ E

then x in A \/ B by XBOOLE_0:def 3;
then x in (A \/ B) \/ C by XBOOLE_0:def 3;
then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def 3;
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in C ; :: thesis: x in (((A \/ B) \/ C) \/ D) \/ E

then x in (A \/ B) \/ C by XBOOLE_0:def 3;
then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def 3;
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in D ; :: thesis: x in (((A \/ B) \/ C) \/ D) \/ E

then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def 3;
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in E ; :: thesis: x in (((A \/ B) \/ C) \/ D) \/ E

hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def 3; :: thesis: verum

end;

end;