theorem :: GLIBPRE1:2

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds
( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X6 or not X6 in X7 or not X7 in X8 or not X8 in X1 )