let x be object ; :: according to PBOOLE:def 13 :: 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 over S such that
A2: U0 = A . x and
A3: (Carrier (A,s)) . x = the Sorts of U0 . s by Def9;
U0 is non-empty MSAlgebra over S by A1, A2, Def5;
hence not (Carrier (A,s)) . x is empty by A3; :: thesis: verum