let a, b, c be boolean object ; :: thesis: ((a '&' b) => c) => (a => (b => c)) = 1
A1: ( a = 0 or a = 1 ) by XBOOLEAN:def 3;
A2: ( b = 0 or b = 1 ) by XBOOLEAN:def 3;
( c = 0 or c = 1 ) by XBOOLEAN:def 3;
hence ((a '&' b) => c) => (a => (b => c)) = 1 by A1, A2; :: thesis: verum