take X1 = {(0. X)}; :: thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1 ) )
A1: for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1

proof

let x, y be Element of X; :: thesis: ( x \ y in X1 & y in X1 implies x in X1 )
assume ( x \ y in X1 & y in X1 ) ; :: thesis: x in X1
then ( x \ y = 0. X & y = 0. X ) by TARSKI:def 1;
then x = 0. X by Th2;
hence x in X1 by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for xx being object st xx in X1 holds
xx in the carrier of X

let xx be object ; :: thesis: ( xx in X1 implies xx in the carrier of X )
assume xx in X1 ; :: thesis: xx in the carrier of X
then xx = 0. X by TARSKI:def 1;
hence xx in the carrier of X ; :: thesis: verum

end;

hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1 ) ) by A1, TARSKI:def 1, TARSKI:def 3; :: thesis: verum