let H be Element of QC-WFF ; :: 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 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 Th5;
hence ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional ) by A1, Def11, QC_LANG1:def 18; :: thesis: verum