let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S
for V being Variables of A
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
let A be MSAlgebra over S; :: thesis: for V being Variables of A
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
let V be Variables of A; :: thesis: for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
let s be SortSymbol of S; :: thesis: for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v
let x be set ; :: thesis: ( x in the Sorts of A . s implies for v being Element of V . s holds x <> v )
assume A1: x in the Sorts of A . s ; :: thesis: for v being Element of V . s holds x <> v
let v be Element of V . s; :: thesis: x <> v
V misses the Sorts of A by Def8;
then V . s misses the Sorts of A . s ;
hence x <> v by A1, XBOOLE_0:3; :: thesis: verum