theorem Th3: :: LTLAXIO1:3

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