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

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