let X, x, y be set ; :: thesis: ( [x,y] in RelIncl X implies x c= y )
assume A1: [x,y] in RelIncl X ; :: thesis: x c= y
field (RelIncl X) = X by WELLORD2:def 1;
then ( x in X & y in X ) by A1, RELAT_1:15;
hence x c= y by A1, WELLORD2:def 1; :: thesis: verum