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 \ (y \ x)) \ z in X1 & z in X1 holds
x in X1 ) )
X1 c= the carrier of X ;
hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in X1 & z in X1 holds
x in X1 ) ) ; :: thesis: verum