let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is biconditional holds
Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))
let p be Element of QC-WFF A; :: thesis: for V being non empty Subset of (QC-variables A) st p is biconditional holds
Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))
let V be non empty Subset of (QC-variables A); :: thesis: ( p is biconditional implies Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V)) )
set p1 = the_left_side_of p;
set p2 = the_right_side_of p;
assume p is biconditional ; :: thesis: Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))
then p = (the_left_side_of p) <=> (the_right_side_of p) by QC_LANG2:39;
then p = ((the_left_side_of p) => (the_right_side_of p)) '&' ((the_right_side_of p) => (the_left_side_of p)) by QC_LANG2:def 4;
hence Vars (p,V) = (Vars (((the_left_side_of p) => (the_right_side_of p)),V)) \/ (Vars (((the_right_side_of p) => (the_left_side_of p)),V)) by Th42
.= ((Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))) \/ (Vars (((the_right_side_of p) => (the_left_side_of p)),V)) by Th48
.= ((Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))) \/ ((Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))) by Th48
.= (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V)) ;
:: thesis: verum