set x = the sample of D;
A1: the sample of D in { the sample of D} by TARSKI:def 1;
reconsider X = { the sample of D} as non empty Element of bool S ;
take X ; :: thesis: ex x being sample of D st x in X
thus ex x being sample of D st x in X by A1; :: thesis: verum