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