set A = <=6n+1 1;
set B = {0,1,2,3,4,5,6,7};
let x be Nat; :: according to MEMBERED:def 18 :: thesis: ( ( not x in <=6n+1 1 or x in {0,1,2,3,4,5,6,7} ) & ( not x in {0,1,2,3,4,5,6,7} or x in <=6n+1 1 ) )

hereby :: thesis: ( not x in {0,1,2,3,4,5,6,7} or x in <=6n+1 1 )

assume x in <=6n+1 1 ; :: thesis: x in {0,1,2,3,4,5,6,7}
then consider a being Nat such that
A1: a = x and
A2: a <= (6 * 1) + 1 ;
not not a = 0 & ... & not a = 7 by A2;
hence x in {0,1,2,3,4,5,6,7} by A1, ENUMSET1:def 6; :: thesis: verum

end;

assume x in {0,1,2,3,4,5,6,7} ; :: thesis: x in <=6n+1 1
then ( x = 0 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 ) by ENUMSET1:def 6;
hence x in <=6n+1 1 ; :: thesis: verum