let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A holds
( the_left_side_of (F <=> G) = F & the_right_side_of (F <=> G) = G & the_left_argument_of (F <=> G) = F => G & the_right_argument_of (F <=> G) = G => F )
let F, G be Element of QC-WFF A; :: thesis: ( the_left_side_of (F <=> G) = F & the_right_side_of (F <=> G) = G & the_left_argument_of (F <=> G) = F => G & the_right_argument_of (F <=> G) = G => F )
( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G ) by Th30;
hence ( the_left_side_of (F <=> G) = F & the_right_side_of (F <=> G) = G & the_left_argument_of (F <=> G) = F => G & the_right_argument_of (F <=> G) = G => F ) by Th4; :: thesis: verum