let X, Y be Subset of CQC-WFF ; :: thesis: still_not-bound_in (X \/ Y) = (still_not-bound_in X) \/ (still_not-bound_in Y)
thus still_not-bound_in (X \/ Y) c= (still_not-bound_in X) \/ (still_not-bound_in Y) :: according to XBOOLE_0:def 10 :: thesis: (still_not-bound_in X) \/ (still_not-bound_in Y) c= still_not-bound_in (X \/ Y)

proof

set A = { (still_not-bound_in p) where p is Element of CQC-WFF : p in X \/ Y } ;
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in still_not-bound_in (X \/ Y) or b in (still_not-bound_in X) \/ (still_not-bound_in Y) )
assume A1: b in still_not-bound_in (X \/ Y) ; :: thesis: b in (still_not-bound_in X) \/ (still_not-bound_in Y)
consider a being set such that
A2: ( b in a & a in { (still_not-bound_in p) where p is Element of CQC-WFF : p in X \/ Y } ) by A1, TARSKI:def 4;
consider p being Element of CQC-WFF such that
A3: ( a = still_not-bound_in p & p in X \/ Y ) by A2;

A4: now

assume p in X ; :: thesis: b in (still_not-bound_in X) \/ (still_not-bound_in Y)
then a in { (still_not-bound_in q) where q is Element of CQC-WFF : q in X } by A3;
then A5: b in union { (still_not-bound_in q) where q is Element of CQC-WFF : q in X } by A2, TARSKI:def 4;
still_not-bound_in X c= (still_not-bound_in X) \/ (still_not-bound_in Y) by XBOOLE_1:7;
hence b in (still_not-bound_in X) \/ (still_not-bound_in Y) by A5; :: thesis: verum

end;

now

assume p in Y ; :: thesis: b in (still_not-bound_in X) \/ (still_not-bound_in Y)
then a in { (still_not-bound_in q) where q is Element of CQC-WFF : q in Y } by A3;
then A6: b in union { (still_not-bound_in q) where q is Element of CQC-WFF : q in Y } by A2, TARSKI:def 4;
still_not-bound_in Y c= (still_not-bound_in X) \/ (still_not-bound_in Y) by XBOOLE_1:7;
hence b in (still_not-bound_in X) \/ (still_not-bound_in Y) by A6; :: thesis: verum

end;

hence b in (still_not-bound_in X) \/ (still_not-bound_in Y) by A3, A4, XBOOLE_0:def 3; :: thesis: verum

end;

thus (still_not-bound_in X) \/ (still_not-bound_in Y) c= still_not-bound_in (X \/ Y) :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in (still_not-bound_in X) \/ (still_not-bound_in Y) or b in still_not-bound_in (X \/ Y) )
assume A7: b in (still_not-bound_in X) \/ (still_not-bound_in Y) ; :: thesis: b in still_not-bound_in (X \/ Y)

A8: now

assume b in still_not-bound_in X ; :: thesis: b in still_not-bound_in (X \/ Y)
then consider a being set such that
A9: ( b in a & a in { (still_not-bound_in p) where p is Element of CQC-WFF : p in X } ) by TARSKI:def 4;
consider p being Element of CQC-WFF such that
A10: ( a = still_not-bound_in p & p in X ) by A9;
X c= X \/ Y by XBOOLE_1:7;
then a in { (still_not-bound_in q) where q is Element of CQC-WFF : q in X \/ Y } by A10;
hence b in still_not-bound_in (X \/ Y) by A9, TARSKI:def 4; :: thesis: verum

end;

now

assume b in still_not-bound_in Y ; :: thesis: b in still_not-bound_in (X \/ Y)
then consider a being set such that
A11: ( b in a & a in { (still_not-bound_in p) where p is Element of CQC-WFF : p in Y } ) by TARSKI:def 4;
consider p being Element of CQC-WFF such that
A12: ( a = still_not-bound_in p & p in Y ) by A11;
Y c= X \/ Y by XBOOLE_1:7;
then a in { (still_not-bound_in q) where q is Element of CQC-WFF : q in X \/ Y } by A12;
hence b in still_not-bound_in (X \/ Y) by A11, TARSKI:def 4; :: thesis: verum

end;

hence b in still_not-bound_in (X \/ Y) by A7, A8, XBOOLE_0:def 3; :: thesis: verum

end;