thus not GRZ-symbols is trivial by Th1; :: thesis: GRZ-symbols is antichain-like
let p be FinSequence; :: according to POLNOT_1:def 16 :: thesis: for b1 being set holds
( not p in GRZ-symbols or not p ^ b1 in GRZ-symbols or b1 = {} )
let q be FinSequence; :: thesis: ( not p in GRZ-symbols or not p ^ q in GRZ-symbols or q = {} )
set r = p ^ q;
assume that
A1: p in GRZ-symbols and
A2: p ^ q in GRZ-symbols ; :: thesis: q = {}
reconsider p = p as Element of GRZ-symbols by A1;
reconsider r = p ^ q as Element of GRZ-symbols by A2;
per cases ( p . 1 = 0 or p . 1 <> 0 ) ;
suppose p . 1 = 0 ; :: thesis: q = {}
then A4: p in VAR by Lm3;
then consider k being Element of NAT such that
A5: p = <*0,k*> ;
r = (<*0*> ^ <*k*>) ^ q by A5, FINSEQ_1:def 9
.= <*0*> ^ (<*k*> ^ q) by FINSEQ_1:32 ;
then r . 1 = 0 by FINSEQ_1:41;
then r in VAR by Lm3;
hence q = {} by A4, POLNOT_1:def 16; :: thesis: verum
end;
suppose A10: p . 1 <> 0 ; :: thesis: q = {}
then not p in VAR by Lm3;
then A11: p in GRZ-ops by XBOOLE_0:def 3;
then dom p = Seg 1 by Lm2;
then 1 in dom p by FINSEQ_1:1;
then r . 1 = p . 1 by FINSEQ_1:def 7;
then not r in VAR by A10, Lm3;
then r in GRZ-ops by XBOOLE_0:def 3;
hence q = {} by A11, POLNOT_1:def 16; :: thesis: verum
end;
end;