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

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