let X be non empty set ; :: thesis: for x, y being Element of (InclPoset X) holds
( x <= y iff x c= y )
let x, y be Element of (InclPoset X); :: thesis: ( x <= y iff x c= y )
thus ( x <= y implies x c= y ) :: thesis: ( x c= y implies x <= y )

proof

assume x <= y ; :: thesis: x c= y
then [x,y] in the InternalRel of (InclPoset X) by ORDERS_2:def 5;
hence x c= y by WELLORD2:def 1; :: thesis: verum

end;

thus ( x c= y implies x <= y ) :: thesis: verum

proof

assume x c= y ; :: thesis: x <= y
then [x,y] in RelIncl X by WELLORD2:def 1;
hence x <= y by ORDERS_2:def 5; :: thesis: verum

end;