let X be set ; :: thesis: ( RelIncl X is finite implies X is finite )
set R = RelIncl X;
assume RelIncl X is finite ; :: thesis: X is finite
then reconsider A = RelIncl X as finite Relation ;
field A is finite ;
hence X is finite by WELLORD2:def 1; :: thesis: verum