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 6 :: 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 Th68;
set c = a => b;
A3: H₁( latt (L,[#p,q#])) = [#p,q#] by Th72;
then p [= a by A2, Th62;
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 7;
p [= b by A2, A3, Th62;
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:5;
then ( ((a => b) "\/" p) "/\" q [= q & p [= ((a => b) "\/" p) "/\" q ) by A2, FILTER_0:7, LATTICES:6;
then reconsider d9 = ((a => b) "\/" p) "/\" q as Element of (latt (L,[#p,q#])) by A2, A3, Th62;
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 Th73, LATTICES:def 7;
hence a9 "/\" d9 [= b9 by A4, A6, Th74; :: 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 Th68;
e [= q by A2, A3, Th62;
then A7: e = e "/\" q by LATTICES:4;
assume a9 "/\" e9 [= b9 ; :: thesis: e9 [= d9
then ae [= b by Th74;
then a "/\" e [= b by Th73;
then A8: e [= a => b by A1, FILTER_0:def 7;
p [= e by A2, A3, Th62;
then e = e "\/" p ;
then e [= (a => b) "\/" p by A8, FILTER_0:1;
then e [= ((a => b) "\/" p) "/\" q by A7, LATTICES:9;
hence e9 [= d9 by Th74; :: thesis: verum