let L be non empty Boolean RelStr ; :: thesis: for a, b being Element of L holds
( 'not' (a "\/" b) = ('not' a) "/\" ('not' b) & 'not' (a "/\" b) = ('not' a) "\/" ('not' b) )
let a, b be Element of L; :: thesis: ( 'not' (a "\/" b) = ('not' a) "/\" ('not' b) & 'not' (a "/\" b) = ('not' a) "\/" ('not' b) )
A1: (a "\/" b) "/\" (('not' a) "/\" ('not' b)) = ((a "\/" b) "/\" ('not' a)) "/\" ('not' b) by LATTICE3:16
.= ((('not' a) "/\" a) "\/" (('not' a) "/\" b)) "/\" ('not' b) by WAYBEL_1:def 3
.= ((Bottom L) "\/" (('not' a) "/\" b)) "/\" ('not' b) by Th34
.= (('not' a) "/\" b) "/\" ('not' b) by WAYBEL_1:3
.= ('not' a) "/\" (b "/\" ('not' b)) by LATTICE3:16
.= ('not' a) "/\" (Bottom L) by Th34
.= Bottom L by WAYBEL_1:3 ;
(a "\/" b) "\/" (('not' a) "/\" ('not' b)) = a "\/" (b "\/" (('not' a) "/\" ('not' b))) by LATTICE3:14
.= a "\/" ((b "\/" ('not' a)) "/\" (b "\/" ('not' b))) by Th17
.= a "\/" ((b "\/" ('not' a)) "/\" (Top L)) by Th34
.= a "\/" (b "\/" ('not' a)) by WAYBEL_1:4
.= (a "\/" ('not' a)) "\/" b by LATTICE3:14
.= (Top L) "\/" b by Th34
.= Top L by WAYBEL_1:4 ;
then ('not' a) "/\" ('not' b) is_a_complement_of a "\/" b by A1, WAYBEL_1:def 23;
hence 'not' (a "\/" b) = ('not' a) "/\" ('not' b) by Th11; :: thesis: 'not' (a "/\" b) = ('not' a) "\/" ('not' b)
A2: (a "/\" b) "/\" (('not' a) "\/" ('not' b)) = a "/\" (b "/\" (('not' a) "\/" ('not' b))) by LATTICE3:16
.= a "/\" ((b "/\" ('not' a)) "\/" (b "/\" ('not' b))) by WAYBEL_1:def 3
.= a "/\" ((b "/\" ('not' a)) "\/" (Bottom L)) by Th34
.= a "/\" (b "/\" ('not' a)) by WAYBEL_1:3
.= (a "/\" ('not' a)) "/\" b by LATTICE3:16
.= (Bottom L) "/\" b by Th34
.= Bottom L by WAYBEL_1:3 ;
(a "/\" b) "\/" (('not' a) "\/" ('not' b)) = ((a "/\" b) "\/" ('not' a)) "\/" ('not' b) by LATTICE3:14
.= ((('not' a) "\/" a) "/\" (('not' a) "\/" b)) "\/" ('not' b) by Th17
.= ((Top L) "/\" (('not' a) "\/" b)) "\/" ('not' b) by Th34
.= (('not' a) "\/" b) "\/" ('not' b) by WAYBEL_1:4
.= ('not' a) "\/" (b "\/" ('not' b)) by LATTICE3:14
.= ('not' a) "\/" (Top L) by Th34
.= Top L by WAYBEL_1:4 ;
then ('not' a) "\/" ('not' b) is_a_complement_of a "/\" b by A2, WAYBEL_1:def 23;
hence 'not' (a "/\" b) = ('not' a) "\/" ('not' b) by Th11; :: thesis: verum