let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q being Polynomial of n,L holds
( p <= q,T iff not q < p,T )
let T be connected TermOrder of n; :: thesis: for L being non empty addLoopStr
for p, q being Polynomial of n,L holds
( p <= q,T iff not q < p,T )
let L be non empty addLoopStr ; :: thesis: for p, q being Polynomial of n,L holds
( p <= q,T iff not q < p,T )
let p, q be Polynomial of n,L; :: thesis: ( p <= q,T iff not q < p,T )
A1: ( not q < p,T implies p <= q,T )

proof

assume A2: not q < p,T ; :: thesis: p <= q,T

now :: thesis: ( ( not Support q <> Support p & p <= q,T ) or ( not q <= p,T & p <= q,T ) )

per cases ( not Support q <> Support p or not q <= p,T ) by A2;

case not Support q <> Support p ; :: thesis: p <= q,T

hence p <= q,T by Th26; :: thesis: verum

end;

case not q <= p,T ; :: thesis: p <= q,T

hence p <= q,T by Th28; :: thesis: verum

end;

end;

end;

hence p <= q,T ; :: thesis: verum

end;

( p <= q,T implies not q < p,T ) by Th26;
hence ( p <= q,T iff not q < p,T ) by A1; :: thesis: verum