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: ( p <= q,T implies not q < p,T )
proof
assume A2: p <= q,T ; :: thesis: not q < p,T
assume A3: q < p,T ; :: thesis: contradiction
then q <= p,T by Def3;
then Support q = Support p by A2, Th26;
hence contradiction by A3, Def3; :: thesis: verum
end;
( not q < p,T implies p <= q,T )
proof
assume A4: not q < p,T ; :: thesis: p <= q,T
now
per cases ( not Support q <> Support p or not q <= p,T ) by A4, Def3;
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;
hence ( p <= q,T iff not q < p,T ) by A1; :: thesis: verum