let H be non empty RelStr ; :: thesis: ( H is Heyting implies for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c) )
assume A1: H is Heyting ; :: thesis: for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c)
then A2: H is LATTICE ;
A3: H is distributive by A1;
let a, b, c be Element of H; :: thesis: (a "\/" b) => c = (a => c) "/\" (b => c)
( a <= a "\/" b & b <= a "\/" b ) by A2, YELLOW_0:22;
then ( (a "\/" b) => c <= a => c & (a "\/" b) => c <= b => c ) by A1, Th78;
then A4: (a "\/" b) => c <= (a => c) "/\" (b => c) by A2, YELLOW_0:23;
set d = (a => c) "/\" (b => c);
A5: (a "\/" b) "/\" ((a => c) "/\" (b => c)) = ((a => c) "/\" (b => c)) "/\" (a "\/" b) by A2, LATTICE3:15
.= (((a => c) "/\" (b => c)) "/\" a) "\/" (((a => c) "/\" (b => c)) "/\" b) by A3, Def3
.= (a "/\" ((a => c) "/\" (b => c))) "\/" (((a => c) "/\" (b => c)) "/\" b) by A2, LATTICE3:15
.= (a "/\" ((a => c) "/\" (b => c))) "\/" (b "/\" ((a => c) "/\" (b => c))) by A2, LATTICE3:15
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((a => c) "/\" (b => c))) by A2, LATTICE3:16
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((b => c) "/\" (a => c))) by A2, LATTICE3:15
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c)) by A2, LATTICE3:16
.= ((a "/\" c) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c)) by A1, Th80
.= ((a "/\" c) "/\" (b => c)) "\/" ((b "/\" c) "/\" (a => c)) by A1, Th80 ;
( (a "/\" c) "/\" (b => c) <= a "/\" c & a "/\" c <= c ) by A2, YELLOW_0:23;
then A6: (a "/\" c) "/\" (b => c) <= c by A2, ORDERS_2:26;
( (b "/\" c) "/\" (a => c) <= b "/\" c & b "/\" c <= c ) by A2, YELLOW_0:23;
then (b "/\" c) "/\" (a => c) <= c by A2, ORDERS_2:26;
then (a "\/" b) "/\" ((a => c) "/\" (b => c)) <= c by A2, A5, A6, YELLOW_0:22;
then (a "\/" b) => c >= (a => c) "/\" (b => c) by A1, Th70;
hence (a "\/" b) => c = (a => c) "/\" (b => c) by A2, A4, ORDERS_2:25; :: thesis: verum