set I = the carrier of S \ the carrier of J;
set Z = the V2() 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 V2() 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 . b1 is empty )
assume s in the carrier of S ; :: thesis: not the Sorts of Q . b1 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 . b1 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 . b1 is empty
then the Sorts of Q . s = the V2() 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 V2() ;
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