let X1 be non empty set ; :: thesis: X1 = { x1 where x1 is Element of X1 : verum }
defpred S₁[ set ] means verum;
A1: for y1 being Element of X1 holds y1 in { x1 where x1 is Element of X1 : verum } ;
{ x1 where x1 is Element of X1 : S₁[x1] } is Subset of X1 from DOMAIN_1:sch 7();
hence X1 = { x1 where x1 is Element of X1 : verum } by A1, SUBSET_1:28; :: thesis: verum