:: deftheorem Def8 defines c< XBOOLE_0:def 8 :
for X, Y being set holds
( X c< Y iff ( X c= Y & X <> Y ) );