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

x in X1 ) ) by A1, TARSKI:def 1, TARSKI:def 3; :: thesis: verum

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;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

now :: thesis: for xx being object st xx in X1 holds

xx in the carrier of X

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 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;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

x in X1 ) ) by A1, TARSKI:def 1, TARSKI:def 3; :: thesis: verum