for X, Y, Z, x being set holds
( x in (X \/ Y) \/ Z iff ( x in X or x in Y or x in Z ) ) by Lm8;