let L be bounded LATTICE; :: thesis: ( ( for x being Element of L ex x' being Element of L st
for y being Element of L holds
( (y "\/" x') "/\" x <= y & y <= (y "/\" x) "\/" x' ) ) implies ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) )
defpred S₁[ Element of L, Element of L] means for y being Element of L holds
( (y "\/" $2) "/\" $1 <= y & y <= (y "/\" $1) "\/" $2 );
assume A1: for x being Element of L ex x' being Element of L st S₁[x,x'] ; :: thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )
consider g' being Function of L,L such that
A2: for x being Element of L holds S₁[x,g' . x] from FUNCT_2:sch 3(A1);

A3: now

let y be Element of L; :: thesis: for g being Function of L,L st ( for z being Element of L holds g . z = (g' . y) "\/" z ) holds
[g,(y "/\" )] is Galois
let g be Function of L,L; :: thesis: ( ( for z being Element of L holds g . z = (g' . y) "\/" z ) implies [g,(y "/\" )] is Galois )
assume A4: for z being Element of L holds g . z = (g' . y) "\/" z ; :: thesis: [g,(y "/\" )] is Galois
A5: g is monotone

proof

let z1, z2 be Element of L; :: according to WAYBEL_1:def 2 :: thesis: ( z1 <= z2 implies g . z1 <= g . z2 )
assume z1 <= z2 ; :: thesis: g . z1 <= g . z2
then (g' . y) "\/" z1 <= z2 "\/" (g' . y) by Th3;
then g . z1 <= (g' . y) "\/" z2 by A4;
hence g . z1 <= g . z2 by A4; :: thesis: verum

end;

now

let x, z be Element of L; :: thesis: ( ( x <= g . z implies (y "/\" ) . x <= z ) & ( (y "/\" ) . x <= z implies x <= g . z ) )

hereby :: thesis: ( (y "/\" ) . x <= z implies x <= g . z )

assume x <= g . z ; :: thesis: (y "/\" ) . x <= z
then x <= (g' . y) "\/" z by A4;
then A6: x "/\" y <= ((g' . y) "\/" z) "/\" y by Th2;
((g' . y) "\/" z) "/\" y <= z by A2;
then x "/\" y <= z by A6, ORDERS_2:26;
hence (y "/\" ) . x <= z by Def18; :: thesis: verum

end;

assume (y "/\" ) . x <= z ; :: thesis: x <= g . z
then y "/\" x <= z by Def18;
then A7: (x "/\" y) "\/" (g' . y) <= z "\/" (g' . y) by Th3;
x <= (x "/\" y) "\/" (g' . y) by A2;
then x <= z "\/" (g' . y) by A7, ORDERS_2:26;
hence x <= g . z by A4; :: thesis: verum

end;

hence [g,(y "/\" )] is Galois by A5, Th9; :: thesis: verum

end;

thus A8: L is Heyting :: thesis: for x being Element of L holds 'not' ('not' x) = x

proof

thus L is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis: for x being Element of L holds x "/\" is lower_adjoint
let y be Element of L; :: thesis: y "/\" is lower_adjoint
deffunc H₁( Element of L) -> M2(the carrier of L) = (g' . y) "\/" $1;
consider g being Function of L,L such that
A9: for z being Element of L holds g . z = H₁(z) from FUNCT_2:sch 4();
[g,(y "/\" )] is Galois by A3, A9;
hence y "/\" is lower_adjoint by Def12; :: thesis: verum

end;

then A10: L is distributive ;

A11: now

let x be Element of L; :: thesis: 'not' x = g' . x
deffunc H₁( Element of L) -> M2(the carrier of L) = (g' . x) "\/" $1;
consider g being Function of L,L such that
A12: for z being Element of L holds g . z = H₁(z) from FUNCT_2:sch 4();
[g,(x "/\" )] is Galois by A3, A12;
then g = x => by A8, Def20;
hence 'not' x = (Bottom L) "\/" (g' . x) by A12
.= g' . x by Th4 ;
:: thesis: verum

end;

A13: now

let x be Element of L; :: thesis: Top L = x "\/" ('not' x)
Top L <= ((Top L) "/\" x) "\/" (g' . x) by A2;
then A14: Top L <= x "\/" (g' . x) by Th5;
x "\/" (g' . x) <= Top L by YELLOW_0:45;
hence Top L = x "\/" (g' . x) by A14, ORDERS_2:25
.= x "\/" ('not' x) by A11 ;
:: thesis: verum

end;

A15: now

let x be Element of L; :: thesis: Bottom L = x "/\" ('not' x)
((Bottom L) "\/" (g' . x)) "/\" x <= Bottom L by A2;
then (x "/\" (Bottom L)) "\/" (x "/\" (g' . x)) <= Bottom L by A10, Def3;
then (Bottom L) "\/" (x "/\" (g' . x)) <= Bottom L by Th4;
then A16: x "/\" (g' . x) <= Bottom L by Th4;
Bottom L <= x "/\" (g' . x) by YELLOW_0:44;
hence Bottom L = x "/\" (g' . x) by A16, ORDERS_2:25
.= x "/\" ('not' x) by A11 ;
:: thesis: verum

end;

let x be Element of L; :: thesis: 'not' ('not' x) = x
(('not' x) "\/" ('not' ('not' x))) "/\" x = (Top L) "/\" x by A13;
then x = x "/\" (('not' x) "\/" ('not' ('not' x))) by Th5
.= (x "/\" ('not' x)) "\/" (x "/\" ('not' ('not' x))) by A10, Def3
.= (Bottom L) "\/" (x "/\" ('not' ('not' x))) by A15
.= x "/\" ('not' ('not' x)) by Th4 ;
then A17: x <= 'not' ('not' x) by YELLOW_0:25;
(Bottom L) "\/" x = (('not' x) "/\" ('not' ('not' x))) "\/" x by A15;
then x = x "\/" (('not' x) "/\" ('not' ('not' x))) by Th4
.= (x "\/" ('not' x)) "/\" (x "\/" ('not' ('not' x))) by A10, Th6
.= (Top L) "/\" (x "\/" ('not' ('not' x))) by A13
.= x "\/" ('not' ('not' x)) by Th5 ;
hence 'not' ('not' x) = x by A17, YELLOW_0:24; :: thesis: verum