let C be initialized ConstructorSignature; :: thesis: for T being quasi-type of C
for a being quasi-adjective of C holds a ast (a ast T) = a ast T
let T be quasi-type of C; :: thesis: for a being quasi-adjective of C holds a ast (a ast T) = a ast T
let a be quasi-adjective of C; :: thesis: a ast (a ast T) = a ast T
thus a ast (a ast T) = [({a} \/ ({a} \/ (adjs T))),(the_base_of (a ast T))]
.= [(({a} \/ {a}) \/ (adjs T)),(the_base_of (a ast T))] by XBOOLE_1:4
.= a ast T ; :: thesis: verum