let x, y, X be set ; :: thesis: ( [x,y] in RelIncl X implies x c= y )
assume Z0: [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 Z0, RELAT_1:15;
hence x c= y by Z0, WELLORD2:def 1; :: thesis: verum