let Al be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF Al) holds still_not-bound_in (X \/ Y) = (still_not-bound_in X) \/ (still_not-bound_in Y)
let X, Y be Subset of (CQC-WFF Al); :: 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 Al : p in X \/ Y } ;
let b be object ; :: 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 b in still_not-bound_in (X \/ Y) ; :: thesis: b in (still_not-bound_in X) \/ (still_not-bound_in Y)
then consider a being set such that
A1: b in a and
A2: a in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X \/ Y } by TARSKI:def 4;
consider p being Element of CQC-WFF Al such that
A3: a = still_not-bound_in p and
A4: p in X \/ Y by A2;
A5: now :: thesis: ( p in X implies b in (still_not-bound_in X) \/ (still_not-bound_in Y) )
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 Al : q in X } by A3;
then A6: b in union { (still_not-bound_in q) where q is Element of CQC-WFF Al : q in X } by A1, 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 A6; :: thesis: verum
end;
now :: thesis: ( p in Y implies b in (still_not-bound_in X) \/ (still_not-bound_in Y) )
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 Al : q in Y } by A3;
then A7: b in union { (still_not-bound_in q) where q is Element of CQC-WFF Al : q in Y } by A1, 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 A7; :: thesis: verum
end;
hence b in (still_not-bound_in X) \/ (still_not-bound_in Y) by A4, A5, 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 object ; :: 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 A8: b in (still_not-bound_in X) \/ (still_not-bound_in Y) ; :: thesis: b in still_not-bound_in (X \/ Y)
A9: now :: thesis: ( b in still_not-bound_in X implies b in still_not-bound_in (X \/ Y) )
assume b in still_not-bound_in X ; :: thesis: b in still_not-bound_in (X \/ Y)
then consider a being set such that
A10: ( b in a & a in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } ) by TARSKI:def 4;
A11: ex p being Element of CQC-WFF Al st
( a = still_not-bound_in p & p in X ) by A10;
X c= X \/ Y by XBOOLE_1:7;
then a in { (still_not-bound_in q) where q is Element of CQC-WFF Al : q in X \/ Y } by A11;
hence b in still_not-bound_in (X \/ Y) by A10, TARSKI:def 4; :: thesis: verum
end;
now :: thesis: ( b in still_not-bound_in Y implies b in still_not-bound_in (X \/ Y) )
assume b in still_not-bound_in Y ; :: thesis: b in still_not-bound_in (X \/ Y)
then consider a being set such that
A12: ( b in a & a in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in Y } ) by TARSKI:def 4;
A13: ex p being Element of CQC-WFF Al st
( a = still_not-bound_in p & p in Y ) by A12;
Y c= X \/ Y by XBOOLE_1:7;
then a in { (still_not-bound_in q) where q is Element of CQC-WFF Al : q in X \/ Y } by A13;
hence b in still_not-bound_in (X \/ Y) by A12, TARSKI:def 4; :: thesis: verum
end;
hence b in still_not-bound_in (X \/ Y) by A8, A9, XBOOLE_0:def 3; :: thesis: verum
end;