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: Bottom H <= Bottom H by ORDERS_2:1;
let a, b be Element of H; :: thesis: 'not' (a "/\" b) >= ('not' a) "\/" ('not' b)
A3: 'not' a <= 'not' a by A1, ORDERS_2:1;
A4: 'not' b <= 'not' b by A1, ORDERS_2:1;
(a "/\" b) "/\" (('not' a) "\/" ('not' b)) = ((a "/\" b) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' b)) by A1, Def3
.= ((b "/\" a) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' b)) by A1, LATTICE3:15
.= (b "/\" (a "/\" ('not' a))) "\/" ((a "/\" b) "/\" ('not' b)) by A1, LATTICE3:16
.= (b "/\" (a "/\" ('not' a))) "\/" (a "/\" (b "/\" ('not' b))) by A1, LATTICE3:16
.= (b "/\" (Bottom H)) "\/" (a "/\" (b "/\" ('not' b))) by A1, A3, Th82
.= (b "/\" (Bottom H)) "\/" (a "/\" (Bottom H)) by A1, A4, Th82
.= ((Bottom H) "/\" b) "\/" (a "/\" (Bottom H)) by A1, LATTICE3:15
.= ((Bottom H) "/\" b) "\/" ((Bottom H) "/\" a) by A1, LATTICE3:15
.= (Bottom H) "\/" ((Bottom H) "/\" a) by A1, Th3
.= (Bottom H) "\/" (Bottom H) by A1, Th3
.= Bottom H by A1, A2, YELLOW_0:24 ;
hence 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) by A1, Th82; :: thesis: verum