let L be Lattice; :: thesis: for p, q being Element of L st L is implicative & p [= q holds
latt L,[#p,q#] is implicative
let p, q be Element of L; :: thesis: ( L is implicative & p [= q implies latt L,[#p,q#] is implicative )
assume A1: L is implicative ; :: thesis: ( not p [= q or latt L,[#p,q#] is implicative )
set P = [#p,q#];
set K = latt L,[#p,q#];
assume A2: p [= q ; :: thesis: latt L,[#p,q#] is implicative
let a9, b9 be Element of (latt L,[#p,q#]); :: according to FILTER_0:def 7 :: thesis: ex b₁ being Element of the carrier of (latt L,[#p,q#]) st
( a9 "/\" b₁ [= b9 & ( for b₂ being Element of the carrier of (latt L,[#p,q#]) holds
( not a9 "/\" b₂ [= b9 or b₂ [= b₁ ) ) )
reconsider a = a9, b = b9 as Element of L by Th69;
set c = a => b;
A3: H₁( latt L,[#p,q#]) = [#p,q#] by Th73;
then p [= a by A2, Th63;
then A4: p "\/" ((a => b) "/\" a) = (p "\/" (a => b)) "/\" a by A1, LATTICES:def 12;
A5: a "/\" (a => b) [= b by A1, FILTER_0:def 8;
p [= b by A2, A3, Th63;
then p "\/" (a "/\" (a => b)) [= b by A5, FILTER_0:6;
then A6: (p "\/" (a "/\" (a => b))) "/\" q [= b by FILTER_0:2;
set d = ((a => b) "\/" p) "/\" q;
p [= (a => b) "\/" p by LATTICES:22;
then ( ((a => b) "\/" p) "/\" q [= q & p [= ((a => b) "\/" p) "/\" q ) by A2, FILTER_0:7, LATTICES:23;
then reconsider d9 = ((a => b) "\/" p) "/\" q as Element of (latt L,[#p,q#]) by A2, A3, Th63;
take d9 ; :: thesis: ( a9 "/\" d9 [= b9 & ( for b₁ being Element of the carrier of (latt L,[#p,q#]) holds
( not a9 "/\" b₁ [= b9 or b₁ [= d9 ) ) )
( ((p "\/" (a => b)) "/\" a) "/\" q = a "/\" (((a => b) "\/" p) "/\" q) & a "/\" (((a => b) "\/" p) "/\" q) = a9 "/\" d9 ) by Th74, LATTICES:def 7;
hence a9 "/\" d9 [= b9 by A4, A6, Th75; :: thesis: for b₁ being Element of the carrier of (latt L,[#p,q#]) holds
( not a9 "/\" b₁ [= b9 or b₁ [= d9 )
let e9 be Element of (latt L,[#p,q#]); :: thesis: ( not a9 "/\" e9 [= b9 or e9 [= d9 )
reconsider e = e9, ae = a9 "/\" e9 as Element of L by Th69;
e [= q by A2, A3, Th63;
then A7: e = e "/\" q by LATTICES:21;
assume a9 "/\" e9 [= b9 ; :: thesis: e9 [= d9
then ae [= b by Th75;
then a "/\" e [= b by Th74;
then A8: e [= a => b by A1, FILTER_0:def 8;
p [= e by A2, A3, Th63;
then e = e "\/" p by LATTICES:def 3;
then e [= (a => b) "\/" p by A8, FILTER_0:1;
then e [= ((a => b) "\/" p) "/\" q by A7, LATTICES:27;
hence e9 [= d9 by Th75; :: thesis: verum