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

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