take X1 = the carrier of X; :: thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in X1 & y in X1 holds
x in X1 ) )
X1 c= X1 ;
hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in X1 & y in X1 holds
x in X1 ) ) ; :: thesis: verum