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