let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A st H is biconditional holds
( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )
let H be Element of QC-WFF A; :: thesis: ( H is biconditional implies ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional ) )
given F, G being Element of QC-WFF A such that A1: H = F <=> G ; :: according to QC_LANG2:def 12 :: thesis: ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )
( the_left_argument_of ((F => G) '&' (G => F)) = F => G & the_right_argument_of ((F => G) '&' (G => F)) = G => F ) by Th4;
hence ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional ) by A1, Def11, QC_LANG1:def 20; :: thesis: verum