theorem Th2: :: LTLAXIO1:2

for a, b, c being boolean object holds (a => (b => c)) => ((a '&' b) => c) = 1