take Y = 1-sorted(# 2 #); :: thesis: ( not Y is trivial & not Y is empty )
thus not Y is trivial :: thesis: not Y is empty

proof

reconsider x = 0 , y = 1 as Element of Y by CARD_1:88, TARSKI:def 2;
take x ; :: according to STRUCT_0:def 10 :: thesis: not for y being Element of Y holds x = y
take y ; :: thesis: not x = y
thus not x = y ; :: thesis: verum

end;

thus not Y is empty ; :: thesis: verum