take Y = 1-sorted(# 2 #); :: thesis: ( not Y is trivial & Y is strict )
reconsider x = 0 , y = 1 as Element of Y by CARD_1:50, TARSKI:def 2;
x <> y ;
hence ( not Y is trivial & Y is strict ) ; :: thesis: verum