for x1, x2, x3, x4, X being set holds
( {x1,x2,x3,x4} c= X iff ( x1 in X & x2 in X & x3 in X & x4 in X ) )