let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L st q <> 0_ (n,L) & HT (p,T) = HT (q,T) & Red (p,T) <= Red (q,T),T holds
p <= q,T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L st q <> 0_ (n,L) & HT (p,T) = HT (q,T) & Red (p,T) <= Red (q,T),T holds
p <= q,T
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of n,L st q <> 0_ (n,L) & HT (p,T) = HT (q,T) & Red (p,T) <= Red (q,T),T holds
p <= q,T
let p, q be Polynomial of n,L; :: thesis: ( q <> 0_ (n,L) & HT (p,T) = HT (q,T) & Red (p,T) <= Red (q,T),T implies p <= q,T )
assume A1: q <> 0_ (n,L) ; :: thesis: ( not HT (p,T) = HT (q,T) or not Red (p,T) <= Red (q,T),T or p <= q,T )
set x = Support (p,T);
set y = Support (q,T);
set rp = Red (p,T);
set rq = Red (q,T);
set R = RelStr(# (Bags n),T #);
assume that
A2: HT (p,T) = HT (q,T) and
A3: Red (p,T) <= Red (q,T),T ; :: thesis: p <= q,T
[(Support (Red (p,T))),(Support (Red (q,T)))] in FinOrd RelStr(# (Bags n),T #) by A3;
then A4: [(Support (Red (p,T))),(Support (Red (q,T)))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by BAGORDER:def 15;
hence p <= q,T ; :: thesis: verum