now :: thesis: Int A is proper

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

end;

hence Int A is proper ; :: thesis: verum