let L be Lattice; :: thesis: for p, q being Element of st L is implicative & p [= q holds
latt L,[#p,q#] is implicative
let p, q be Element of ; :: 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 a', b' be Element of ; :: 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 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 d' = ((a => b) "\/" p) "/\" q as Element of by A2, A3, 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' ) ) )
( ((p "\/" (a => b)) "/\" a) "/\" q = a "/\" (((a => b) "\/" p) "/\" q) & a "/\" (((a => b) "\/" p) "/\" q) = a' "/\" d' ) by Th74, LATTICES:def 7;
hence a' "/\" d' [= b' by A4, 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 ; :: thesis: ( not a' "/\" e' [= b' or e' [= d' )
reconsider e = e', ae = a' "/\" e' as Element of by Th69;
e [= q by A2, A3, Th63;
then A7: e = e "/\" q by LATTICES:21;
assume a' "/\" e' [= b' ; :: thesis: e' [= d'
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 e' [= d' by Th75; :: thesis: verum