let P be Subset of T; :: according to KURATO_1:def 8 :: thesis: ( P in Kurat7Set A implies Int P in Kurat7Set A )
assume P in Kurat7Set A ; :: thesis: Int P in Kurat7Set A
hence Int P in Kurat7Set A by Th10; :: thesis: verum