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 )
then A2: L is I_Lattice ;
assume A3: p [= q ; :: thesis: latt L,[#p,q#] is implicative
set P = [#p,q#];
set K = latt L,[#p,q#];
A4: H₁( latt L,[#p,q#]) = [#p,q#] by Th73;
let a', b' 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
( a' "/\" b₁ [= b' & ( for b₂ being Element of the carrier of (latt L,[#p,q#]) holds
( not a' "/\" b₂ [= b' or b₂ [= b₁ ) ) )
reconsider a = a', b = b' as Element of L by Th69;
A5: ( a [= q & p [= a & b [= q & p [= b ) by A3, A4, Th63;
set c = a => b;
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 A3, FILTER_0:7, LATTICES:23;
then reconsider d' = ((a => b) "\/" p) "/\" q as Element of (latt L,[#p,q#]) by A3, A4, Th63;
take d' ; :: thesis: ( a' "/\" d' [= b' & ( for b₁ being Element of the carrier of (latt L,[#p,q#]) holds
( not a' "/\" b₁ [= b' or b₁ [= d' ) ) )
A6: ( p "\/" ((a => b) "/\" a) = (p "\/" (a => b)) "/\" a & ((p "\/" (a => b)) "/\" a) "/\" q = a "/\" (((a => b) "\/" p) "/\" q) & a "/\" (((a => b) "\/" p) "/\" q) = a' "/\" d' ) by A2, A5, Th74, LATTICES:def 7, LATTICES:def 12;
a "/\" (a => b) [= b by A1, FILTER_0:def 8;
then p "\/" (a "/\" (a => b)) [= b by A5, FILTER_0:6;
then (p "\/" (a "/\" (a => b))) "/\" q [= b by FILTER_0:2;
hence a' "/\" d' [= b' by A6, Th75; :: thesis: for b₁ being Element of the carrier of (latt L,[#p,q#]) holds
( not a' "/\" b₁ [= b' or b₁ [= d' )
let e' be Element of (latt L,[#p,q#]); :: thesis: ( not a' "/\" e' [= b' or e' [= d' )
reconsider e = e', ae = a' "/\" e' as Element of L by Th69;
assume a' "/\" e' [= b' ; :: thesis: e' [= d'
then ae [= b by Th75;
then ( a "/\" e [= b & p [= e ) by A3, A4, Th63, Th74;
then ( e [= a => b & e = e "\/" p & e [= q ) by A1, A3, A4, Th63, FILTER_0:def 8, LATTICES:def 3;
then ( e [= (a => b) "\/" p & e = e "/\" q ) by FILTER_0:1, LATTICES:21;
then e [= ((a => b) "\/" p) "/\" q by LATTICES:27;
hence e' [= d' by Th75; :: thesis: verum