let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L holds BagOrder n linearly_orders Support p
let L be non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds BagOrder n linearly_orders Support p
let p be Polynomial of n,L; :: thesis: BagOrder n linearly_orders Support p
set R = BagOrder n;
( BagOrder n is reflexive & BagOrder n is transitive & BagOrder n is antisymmetric & BagOrder n is connected ) by ORDERS_1:def 5;
then A1: ( BagOrder n is_reflexive_in field (BagOrder n) & BagOrder n is_antisymmetric_in field (BagOrder n) & BagOrder n is_transitive_in field (BagOrder n) & BagOrder n is_connected_in field (BagOrder n) ) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16;
for x being set st x in Bags n holds
x in field (BagOrder n)

proof

let x be set ; :: thesis: ( x in Bags n implies x in field (BagOrder n) )
assume x in Bags n ; :: thesis: x in field (BagOrder n)
then reconsider x = x as bag of by POLYNOM1:def 14;
EmptyBag n <=' x by POLYNOM1:64;
then [(EmptyBag n),x] in BagOrder n by POLYNOM1:def 16;
then A2: x in rng (BagOrder n) by RELAT_1:def 5;
field (BagOrder n) = (dom (BagOrder n)) \/ (rng (BagOrder n)) by RELAT_1:def 6;
then rng (BagOrder n) c= field (BagOrder n) by XBOOLE_1:7;
hence x in field (BagOrder n) by A2; :: thesis: verum

end;

then A3: Bags n c= field (BagOrder n) by TARSKI:def 3;
then A4: Support p c= field (BagOrder n) by XBOOLE_1:1;
A5: ( BagOrder n is_reflexive_in Support p & BagOrder n is_antisymmetric_in Support p & BagOrder n is_transitive_in Support p ) by Lm1;
[:(Bags n),(Bags n):] c= [:(field (BagOrder n)),(field (BagOrder n)):] by A3, ZFMISC_1:119;
then BagOrder n c= [:(field (BagOrder n)),(field (BagOrder n)):] by XBOOLE_1:1;
then reconsider R' = BagOrder n as Relation of (field (BagOrder n)) ;
dom R' = field (BagOrder n) by A1, ORDERS_1:98;
then R' is total by PARTFUN1:def 4;
then R' is_connected_in Support p by A1, A4, Lm2;
hence BagOrder n linearly_orders Support p by A5, ORDERS_1:def 8; :: thesis: verum