A1: support b c= dom b by Th36;
for x being object st x in support b holds
x in X

proof

let x be object ; :: thesis: ( x in support b implies x in X )
assume x in support b ; :: thesis: x in X
then x in dom b by A1;
hence x in X ; :: thesis: verum

end;

hence support b is finite Subset of X by TARSKI:def 3; :: thesis: verum