let H be non empty lower-bounded RelStr ; :: thesis: ( H is Heyting implies for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b)
then A2: H is distributive ;
let a, b be Element of H; :: thesis: 'not' (a "/\" b) >= ('not' a) "\/" ('not' b)
A3: H is LATTICE by A1;
then A4: 'not' a <= 'not' a by ORDERS_2:24;
A5: 'not' b <= 'not' b by A3, ORDERS_2:24;
A6: Bottom H <= Bottom H by A3, ORDERS_2:24;
(a "/\" b) "/\" (('not' a) "\/" ('not' b)) = ((a "/\" b) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' b)) by A2, Def3
.= ((b "/\" a) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' b)) by A3, LATTICE3:15
.= (b "/\" (a "/\" ('not' a))) "\/" ((a "/\" b) "/\" ('not' b)) by A3, LATTICE3:16
.= (b "/\" (a "/\" ('not' a))) "\/" (a "/\" (b "/\" ('not' b))) by A3, LATTICE3:16
.= (b "/\" (Bottom H)) "\/" (a "/\" (b "/\" ('not' b))) by A1, A4, Th85
.= (b "/\" (Bottom H)) "\/" (a "/\" (Bottom H)) by A1, A5, Th85
.= ((Bottom H) "/\" b) "\/" (a "/\" (Bottom H)) by A3, LATTICE3:15
.= ((Bottom H) "/\" b) "\/" ((Bottom H) "/\" a) by A3, LATTICE3:15
.= (Bottom H) "\/" ((Bottom H) "/\" a) by A3, Th4
.= (Bottom H) "\/" (Bottom H) by A3, Th4
.= Bottom H by A3, A6, YELLOW_0:24 ;
hence 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) by A1, Th85; :: thesis: verum