:: deftheorem Def1 defines as_1-sorted YELLOW21:def 1 :
for a being object holds
( ( a is 1-sorted implies a as_1-sorted = a ) & ( a is not 1-sorted implies a as_1-sorted = the 1-sorted ) );