let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A st p is conjunctive holds
( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) )
let p be Element of QC-WFF A; :: thesis: ( p is conjunctive implies ( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) ) )
assume A1: p is conjunctive ; :: thesis: ( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) )
then consider l, q being Element of QC-WFF A such that
A2: p = l '&' q ;
p = <*[2,0]*> ^ ((@ l) ^ (@ q)) by A2, FINSEQ_1:32;
then A3: len (@ p) = (len <*[2,0]*>) + (len ((@ l) ^ (@ q))) by FINSEQ_1:22
.= (len ((@ l) ^ (@ q))) + 1 by FINSEQ_1:40 ;
A4: (len (@ q)) + (len (@ l)) = len ((@ l) ^ (@ q)) by FINSEQ_1:22;
then len (@ q) <= len ((@ l) ^ (@ q)) by NAT_1:11;
then A5: len (@ q) < len (@ p) by A3, NAT_1:13;
len (@ l) <= len ((@ l) ^ (@ q)) by A4, NAT_1:11;
then len (@ l) < len (@ p) by A3, NAT_1:13;
hence ( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) ) by A1, A2, A5, Def25, Def26; :: thesis: verum