let p, q be Element of HP-WFF ; :: thesis: ( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )

hereby :: thesis: ( p in HP_TAUT & q in HP_TAUT implies p '&' q in HP_TAUT )

assume A1: p '&' q in HP_TAUT ; :: thesis: ( p in HP_TAUT & q in HP_TAUT )
( (p '&' q) => p in HP_TAUT & (p '&' q) => q in HP_TAUT ) by Def10;
hence ( p in HP_TAUT & q in HP_TAUT ) by A1, Def10; :: thesis: verum

end;

assume A2: ( p in HP_TAUT & q in HP_TAUT ) ; :: thesis: p '&' q in HP_TAUT
p => (q => (p '&' q)) in HP_TAUT by Def10;
then q => (p '&' q) in HP_TAUT by A2, Def10;
hence p '&' q in HP_TAUT by A2, Def10; :: thesis: verum