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 & (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 A2; :: thesis: verum