let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( Upper_Support p,T,(card (Support p)) = Support p & Lower_Support p,T,(card (Support p)) = {} )
let T be connected TermOrder of n; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( Upper_Support p,T,(card (Support p)) = Support p & Lower_Support p,T,(card (Support p)) = {} )
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds
( Upper_Support p,T,(card (Support p)) = Support p & Lower_Support p,T,(card (Support p)) = {} )
let p be Polynomial of n,L; :: thesis: ( Upper_Support p,T,(card (Support p)) = Support p & Lower_Support p,T,(card (Support p)) = {} )
set u = Upper_Support p,T,(card (Support p));
set l = Lower_Support p,T,(card (Support p));
( Upper_Support p,T,(card (Support p)) c= Support p & card (Upper_Support p,T,(card (Support p))) = card (Support p) ) by Def2;
hence Upper_Support p,T,(card (Support p)) = Support p by TRIANG_1:3; :: thesis: Lower_Support p,T,(card (Support p)) = {}
hence Lower_Support p,T,(card (Support p)) = {} by XBOOLE_1:37; :: thesis: verum