let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum }
let X be V5() ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum }
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: T deg<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum }
thus T deg<= 0 c= { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } :: according to XBOOLE_0:def 10 :: thesis: { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } c= T deg<= 0
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in T deg<= 0 or a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } )
assume a in T deg<= 0 ; :: thesis: a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum }
then consider r being Element of T such that
A1: ( a = r & deg r <= 0 ) ;
A2: ( deg (@ r) = deg r & deg r = 0 ) by A1;
reconsider t = r as Element of (Free (S,X)) by MSAFREE4:39;
( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p ) by Th16;
hence a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } by A1, A2, Th22; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } or a in T deg<= 0 )
assume a in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } ; :: thesis: a in T deg<= 0
then consider s being SortSymbol of S, x being Element of X . s such that
A3: a = x -term ;
( deg (x -term) = 0 & 0 <= 0 & x -term in T ) by Th21, Th24;
then reconsider r = x -term as Element of T ;
( deg r = deg (@ r) & deg (@ r) = 0 ) by Th21;
hence a in T deg<= 0 by A3; :: thesis: verum