theorem Th3: :: YELLOW_1:3

for X being non empty set
for x, y being Element of (InclPoset X) holds
( x <= y iff x c= y )