now

assume not Int A is proper ; :: thesis: contradiction
then A1: Int A = [#] X by SUBSET_1:def 7;
Int A c= A by TOPS_1:44;
hence contradiction by A1, XBOOLE_0:def 10; :: thesis: verum

end;

hence Int A is proper ; :: thesis: verum