theorem :: YELLOW_1:1

for X being set holds
( the carrier of (InclPoset X) = X & the InternalRel of (InclPoset X) = RelIncl X ) ;