now :: thesis: Int A is proper

hence
Int A is proper
; :: thesis: verumassume
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;then A1: Int A = [#] X ;

Int A c= A by TOPS_1:16;

hence contradiction by A1, XBOOLE_0:def 10; :: thesis: verum