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)
let a, b, c be Element of H; :: thesis: (a "\/" b) => c = (a => c) "/\" (b => c)
( (a "/\" c) "/\" (b => c) <= a "/\" c & a "/\" c <= c ) by A1, YELLOW_0:23;
then A2: (a "/\" c) "/\" (b => c) <= c by A1, ORDERS_2:3;
( (b "/\" c) "/\" (a => c) <= b "/\" c & b "/\" c <= c ) by A1, YELLOW_0:23;
then A3: (b "/\" c) "/\" (a => c) <= c by A1, ORDERS_2:3;
set d = (a => c) "/\" (b => c);
(a "\/" b) "/\" ((a => c) "/\" (b => c)) = ((a => c) "/\" (b => c)) "/\" (a "\/" b) by A1, LATTICE3:15
.= (((a => c) "/\" (b => c)) "/\" a) "\/" (((a => c) "/\" (b => c)) "/\" b) by A1, Def3
.= (a "/\" ((a => c) "/\" (b => c))) "\/" (((a => c) "/\" (b => c)) "/\" b) by A1, LATTICE3:15
.= (a "/\" ((a => c) "/\" (b => c))) "\/" (b "/\" ((a => c) "/\" (b => c))) by A1, LATTICE3:15
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((a => c) "/\" (b => c))) by A1, LATTICE3:16
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((b => c) "/\" (a => c))) by A1, LATTICE3:15
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c)) by A1, LATTICE3:16
.= ((a "/\" c) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c)) by A1, Th77
.= ((a "/\" c) "/\" (b => c)) "\/" ((b "/\" c) "/\" (a => c)) by A1, Th77 ;
then (a "\/" b) "/\" ((a => c) "/\" (b => c)) <= c by A1, A2, A3, YELLOW_0:22;
then A4: (a "\/" b) => c >= (a => c) "/\" (b => c) by A1, Th67;
b <= a "\/" b by A1, YELLOW_0:22;
then A5: (a "\/" b) => c <= b => c by A1, Th75;
a <= a "\/" b by A1, YELLOW_0:22;
then (a "\/" b) => c <= a => c by A1, Th75;
then (a "\/" b) => c <= (a => c) "/\" (b => c) by A1, A5, YELLOW_0:23;
hence (a "\/" b) => c = (a => c) "/\" (b => c) by A1, A4, ORDERS_2:2; :: thesis: verum