let L be bounded LATTICE; :: thesis: ( ( for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) 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 x9 being Element of L st S₁[x,x9] ; :: thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )
consider g9 being Function of L,L such that
A2: for x being Element of L holds S₁[x,g9 . x] from FUNCT_2:sch 3(A1);

A3: now :: thesis: for y being Element of L
for g being Function of L,L st ( for z being Element of L holds g . z = (g9 . y) "\/" z ) holds
[g,(y "/\")] is Galois

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

A5: now :: thesis: for x, z being Element of L holds
( ( x <= g . z implies (y "/\") . x <= z ) & ( (y "/\") . x <= z implies x <= g . z ) )

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 <= (g9 . y) "\/" z by A4;
then A6: x "/\" y <= ((g9 . y) "\/" z) "/\" y by Th1;
((g9 . y) "\/" z) "/\" y <= z by A2;
then x "/\" y <= z by A6, ORDERS_2:3;
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) "\/" (g9 . y) <= z "\/" (g9 . y) by Th2;
x <= (x "/\" y) "\/" (g9 . y) by A2;
then x <= z "\/" (g9 . y) by A7, ORDERS_2:3;
hence x <= g . z by A4; :: thesis: verum

end;

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 (g9 . y) "\/" z1 <= z2 "\/" (g9 . y) by Th2;
then g . z1 <= (g9 . y) "\/" z2 by A4;
hence g . z1 <= g . z2 by A4; :: thesis: verum

end;

hence [g,(y "/\")] is Galois by A5; :: 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) -> M3( the carrier of L) = (g9 . 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 ; :: thesis: verum

end;

A10: now :: thesis: for x being Element of L holds 'not' x = g9 . x

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

end;

A12: now :: thesis: for x being Element of L holds Bottom L = x "/\" ('not' x)

let x be Element of L; :: thesis: Bottom L = x "/\" ('not' x)
((Bottom L) "\/" (g9 . x)) "/\" x <= Bottom L by A2;
then (x "/\" (Bottom L)) "\/" (x "/\" (g9 . x)) <= Bottom L by A8, Def3;
then (Bottom L) "\/" (x "/\" (g9 . x)) <= Bottom L by Th3;
then A13: x "/\" (g9 . x) <= Bottom L by Th3;
Bottom L <= x "/\" (g9 . x) by YELLOW_0:44;
hence Bottom L = x "/\" (g9 . x) by A13, ORDERS_2:2
.= x "/\" ('not' x) by A10 ;
:: thesis: verum

end;

let x be Element of L; :: thesis: 'not' ('not' x) = x

A14: now :: thesis: for x being Element of L holds Top L = x "\/" ('not' x)

let x be Element of L; :: thesis: Top L = x "\/" ('not' x)
Top L <= ((Top L) "/\" x) "\/" (g9 . x) by A2;
then A15: Top L <= x "\/" (g9 . x) by Th4;
x "\/" (g9 . x) <= Top L by YELLOW_0:45;
hence Top L = x "\/" (g9 . x) by A15, ORDERS_2:2
.= x "\/" ('not' x) by A10 ;
:: thesis: verum

end;

then (('not' x) "\/" ('not' ('not' x))) "/\" x = (Top L) "/\" x ;
then x = x "/\" (('not' x) "\/" ('not' ('not' x))) by Th4
.= (x "/\" ('not' x)) "\/" (x "/\" ('not' ('not' x))) by A8, Def3
.= (Bottom L) "\/" (x "/\" ('not' ('not' x))) by A12
.= x "/\" ('not' ('not' x)) by Th3 ;
then A16: x <= 'not' ('not' x) by YELLOW_0:25;
(Bottom L) "\/" x = (('not' x) "/\" ('not' ('not' x))) "\/" x by A12;
then x = x "\/" (('not' x) "/\" ('not' ('not' x))) by Th3
.= (x "\/" ('not' x)) "/\" (x "\/" ('not' ('not' x))) by A8, Th5
.= (Top L) "/\" (x "\/" ('not' ('not' x))) by A14
.= x "\/" ('not' ('not' x)) by Th4 ;
hence 'not' ('not' x) = x by A16, YELLOW_0:24; :: thesis: verum