let p be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables 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 ; :: 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:55;
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 Th53
.= ((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 Th59
.= ((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 Th59
.= (Vars (the_left_side_of p),V) \/ (Vars (the_right_side_of p),V) ;
:: thesis: verum