:: deftheorem defines InclPoset YELLOW_1:def 1 :
for X being set holds InclPoset X = RelStr(# X,(RelIncl X) #);