let a be quasi-adjective; :: thesis: for T being quasi-type holds constrs (a ast T) = (constrs a) \/ (constrs T)
let T be quasi-type; :: thesis: constrs (a ast T) = (constrs a) \/ (constrs T)
set A = { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ;
set B = { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ;
A1: { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } = { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)}

proof

thus { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } c= { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} :: according to XBOOLE_0:def 10 :: thesis: { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} c= { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } or z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} )
assume z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ; :: thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)}
then consider a9 being quasi-adjective such that
A2: ( z = constrs a9 & a9 in {a} \/ (adjs T) ) ;
( a9 in {a} or a9 in adjs T ) by A2, XBOOLE_0:def 3;
then ( a9 = a or a9 in adjs T ) by TARSKI:def 1;
then ( z in {(constrs a)} or z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ) by A2, TARSKI:def 1;
hence z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} by XBOOLE_0:def 3; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} or z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } )
assume A3: z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} ; :: thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) }
A4: a in {a} by TARSKI:def 1;

per cases ( z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } or z in {(constrs a)} ) by A3, XBOOLE_0:def 3;

suppose z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ; :: thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) }

then consider a9 being quasi-adjective such that
A5: ( z = constrs a9 & a9 in adjs T ) ;
a9 in {a} \/ (adjs T) by A5, XBOOLE_0:def 3;
hence z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } by A5; :: thesis: verum

end;

suppose z in {(constrs a)} ; :: thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) }

then ( z = constrs a & a in {a} \/ (adjs T) ) by A4, TARSKI:def 1, XBOOLE_0:def 3;
hence z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ; :: thesis: verum

end;

end;

end;

thus constrs (a ast T) = (constrs (the_base_of (a ast T))) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } )
.= (constrs (the_base_of T)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } )
.= (constrs (the_base_of T)) \/ ((union {(constrs a)}) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by A1, ZFMISC_1:78
.= (constrs (the_base_of T)) \/ ((constrs a) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by ZFMISC_1:25
.= ((constrs (the_base_of T)) \/ (constrs a)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ) by XBOOLE_1:4
.= (constrs a) \/ ((constrs (the_base_of T)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by XBOOLE_1:4
.= (constrs a) \/ (constrs T) ; :: thesis: verum