let x, y be LD-EqClass; :: thesis: ( x '&' y is LD-provable iff ( x is LD-provable & y is LD-provable ) )
consider t, u being GRZ-formula such that
A2: ( x = LD-EqClassOf t & y = LD-EqClassOf u ) and
A3: x '&' y = LD-EqClassOf (t '&' u) by Def92;
thus ( x '&' y is LD-provable implies ( x is LD-provable & y is LD-provable ) ) :: thesis: ( x is LD-provable & y is LD-provable implies x '&' y is LD-provable )
proof
assume x '&' y is LD-provable ; :: thesis: ( x is LD-provable & y is LD-provable )
then t '&' u is LD-provable by A3, Th90;
then ( t is LD-provable & u is LD-provable ) by Th60;
hence ( x is LD-provable & y is LD-provable ) by A2; :: thesis: verum
end;
assume ( x is LD-provable & y is LD-provable ) ; :: thesis: x '&' y is LD-provable
then ( t is LD-provable & u is LD-provable ) by A2, Th90;
then t '&' u is LD-provable by Th60;
hence x '&' y is LD-provable by A3; :: thesis: verum