set I = the carrier of S \ the carrier of J;
set Z = the non-empty ManySortedSet of the carrier of S \ the carrier of J;
consider Q being MSAlgebra over S such that
A1: ( Q is T -extension & the Sorts of Q | ( the carrier of S \ the carrier of J) = the non-empty ManySortedSet of the carrier of S \ the carrier of J ) by Th17;

now :: thesis: for s being object st s in the carrier of S holds
not the Sorts of Q . s is empty

let s be object ; :: thesis: ( s in the carrier of S implies not the Sorts of Q . b₁ is empty )
assume s in the carrier of S ; :: thesis: not the Sorts of Q . b₁ is empty

per cases then ( s in the carrier of J or s in the carrier of S \ the carrier of J ) by XBOOLE_0:def 5;

suppose A2: s in the carrier of J ; :: thesis: not the Sorts of Q . b₁ is empty

then the Sorts of Q . s = the Sorts of T . s by A1, Th16;
hence not the Sorts of Q . s is empty by A2; :: thesis: verum

end;

suppose A3: s in the carrier of S \ the carrier of J ; :: thesis: not the Sorts of Q . b₁ is empty

then the Sorts of Q . s = the non-empty ManySortedSet of the carrier of S \ the carrier of J . s by A1, FUNCT_1:49;
hence not the Sorts of Q . s is empty by A3; :: thesis: verum

end;

end;

end;

then the Sorts of Q is non-empty ;
then reconsider Q = Q as non-empty MSAlgebra over S by MSUALG_1:def 3;
take Q ; :: thesis: Q is T -extension
thus Q is T -extension by A1; :: thesis: verum