let p, q be Element of QC-WFF ; for V being non empty Subset of QC-variables holds Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))
let V be non empty Subset of QC-variables; Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))
A1:
the_right_side_of (p <=> q) = q
by QC_LANG2:47;
( p <=> q is biconditional & the_left_side_of (p <=> q) = p )
by QC_LANG2:47, QC_LANG2:def 12;
hence
Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))
by A1, Th60; verum