let Y be non empty set ; :: thesis: for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d
let a, b, c, d be Function of Y,BOOLEAN; :: thesis: ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d
let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = TRUE or (c 'or' d) . z = TRUE )
A1: (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = (((a 'imp' c) '&' (b 'imp' d)) . z) '&' ((a 'or' b) . z) by MARGREL1:def 20
.= (((a 'imp' c) . z) '&' ((b 'imp' d) . z)) '&' ((a 'or' b) . z) by MARGREL1:def 20
.= (((('not' a) 'or' c) . z) '&' ((b 'imp' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_4:8
.= (((('not' a) 'or' c) . z) '&' ((('not' b) 'or' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_4:8
.= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) 'or' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_1:def 4
.= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a 'or' b) . z) by BVFUNC_1:def 4
.= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by BVFUNC_1:def 4
.= ((('not' (a . z)) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by MARGREL1:def 19
.= ((('not' (a . z)) 'or' (c . z)) '&' (('not' (b . z)) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by MARGREL1:def 19 ;
reconsider bz = b . z as boolean object ;
reconsider az = a . z as boolean object ;
assume A2: (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = TRUE ; :: thesis: (c 'or' d) . z = TRUE

now :: thesis: ( (c 'or' d) . z <> TRUE implies (c 'or' d) . z = TRUE )

assume (c 'or' d) . z <> TRUE ; :: thesis: (c 'or' d) . z = TRUE
then (c 'or' d) . z = FALSE by XBOOLEAN:def 3;
then A3: (c . z) 'or' (d . z) = FALSE by BVFUNC_1:def 4;
( d . z = TRUE or d . z = FALSE ) by XBOOLEAN:def 3;
then ((('not' (a . z)) 'or' (c . z)) '&' (('not' (b . z)) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) = ('not' (a . z)) '&' (('not' (b . z)) '&' ((b . z) 'or' (a . z))) by A3
.= ('not' (a . z)) '&' ((('not' bz) '&' bz) 'or' (('not' (b . z)) '&' (a . z))) by XBOOLEAN:8
.= ('not' (a . z)) '&' (FALSE 'or' (('not' (b . z)) '&' (a . z))) by XBOOLEAN:138
.= ('not' (a . z)) '&' ((a . z) '&' ('not' (b . z)))
.= (('not' az) '&' az) '&' ('not' (b . z))
.= FALSE '&' ('not' (b . z)) by XBOOLEAN:138
.= FALSE ;
hence (c 'or' d) . z = TRUE by A2, A1; :: thesis: verum

end;

hence (c 'or' d) . z = TRUE ; :: thesis: verum