let x be set ; :: according to PBOOLE:def 16 :: thesis: ( not x in I or not (Carrier (A,s)) . x is empty )
assume A1: x in I ; :: thesis: not (Carrier (A,s)) . x is empty
then consider U0 being MSAlgebra of S such that
A2: U0 = A . x and
A3: (Carrier (A,s)) . x = the Sorts of U0 . s by Def16;
U0 is non-empty MSAlgebra of S by A1, A2, Def12;
hence not (Carrier (A,s)) . x is empty by A3; :: thesis: verum