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) \ z in X1 & y \ z in X1 holds

x \ z 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) \ z in X1 & y \ z in X1 holds

x \ z in X1 ) ) ; :: thesis: verum

x \ z 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) \ z in X1 & y \ z in X1 holds

x \ z in X1 ) ) ; :: thesis: verum