let L be non empty NelsonStr ; :: thesis: ( L is satisfying_N0* implies ( L is Nelson_Algebra iff ( L is satisfying_N1* & L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* ) ) )
assume A1: L is satisfying_N0* ; :: thesis: ( L is Nelson_Algebra iff ( L is satisfying_N1* & L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* ) )
thus ( L is Nelson_Algebra implies ( L is satisfying_N1* & L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* ) ) ; :: thesis: ( L is satisfying_N1* & L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* implies L is Nelson_Algebra )
assume A2: ( L is satisfying_N1* & L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* ) ; :: thesis: L is Nelson_Algebra
then reconsider L1 = L as non empty DeMorgan NelsonStr ;
A3: for a, b being Element of L1 st a "/\" b = Top L1 holds
( a = Top L1 & b = Top L1 )
proof
let a, b be Element of L1; :: thesis: ( a "/\" b = Top L1 implies ( a = Top L1 & b = Top L1 ) )
assume a "/\" b = Top L1 ; :: thesis: ( a = Top L1 & b = Top L1 )
then ( Top L1 < a & Top L1 < b ) by A2;
hence ( a = Top L1 & b = Top L1 ) by A2; :: thesis: verum
end;
set w = Top L1;
A4: (Top L1) => (Top L1) = Top L1 by A2;
then (Top L1) => (((Top L1) => (Top L1)) => ((Top L1) => ((Top L1) "/\" (Top L1)))) = Top L1 by A2;
then (Top L1) => ((Top L1) => ((Top L1) "/\" (Top L1))) = Top L1 by A4, A2;
then (Top L1) => ((Top L1) "/\" (Top L1)) = Top L1 by A2;
then A5: (Top L1) "/\" (Top L1) = Top L1 by A2;
A6: for a, b being Element of L1 holds
( a <= b iff ( a < b & - b < - a ) )
proof
let a, b be Element of L1; :: thesis: ( a <= b iff ( a < b & - b < - a ) )
A7: a =-> b = (a => b) "/\" ((- b) => (- a)) by A2;
thus ( a <= b implies ( a < b & - b < - a ) ) :: thesis: ( a < b & - b < - a implies a <= b )
proof
assume a <= b ; :: thesis: ( a < b & - b < - a )
then a =-> b = Top L1 by A1;
hence ( a < b & - b < - a ) by A3, A7; :: thesis: verum
end;
assume ( a < b & - b < - a ) ; :: thesis: a <= b
hence a <= b by A7, A5, A1; :: thesis: verum
end;
set d = (Top L) ` ;
A8: for a being Element of L holds a <= Top L
proof
let a be Element of L; :: thesis: a <= Top L
a => (Top L) = (Top L) => (a => (Top L)) by A2;
then A9: a < Top L by A2;
(- (Top L)) => ((Top L) => (- a)) = Top L by A2;
then - (Top L) < - a by A2;
hence a <= Top L by A6, A9; :: thesis: verum
end;
A10: for a being Element of L holds (Top L) ` <= a
proof
let a be Element of L; :: thesis: (Top L) ` <= a
(- (Top L)) => ((Top L) => a) = Top L by A2;
then A11: - (Top L) < a by A2;
- a <= Top L by A8;
then - a < Top L by A2;
then - a < - ((Top L) `) by A2;
hence (Top L) ` <= a by A11, A6; :: thesis: verum
end;
A12: for a being Element of L holds ((Top L) `) "/\" a = (Top L) `
proof
let a be Element of L; :: thesis: ((Top L) `) "/\" a = (Top L) `
(Top L) ` <= a by A10;
hence ((Top L) `) "/\" a = (Top L) ` ; :: thesis: verum
end;
A13: for a being Element of L1 holds a => (Top L1) = Top L1
proof
let a be Element of L1; :: thesis: a => (Top L1) = Top L1
(Top L1) => (a => (Top L1)) = Top L1 by A2;
hence a => (Top L1) = Top L1 by A2; :: thesis: verum
end;
A14: for a, b, c being Element of L1 st a => b = Top L1 & b => c = Top L1 holds
a => c = Top L1
proof
let a, b, c be Element of L1; :: thesis: ( a => b = Top L1 & b => c = Top L1 implies a => c = Top L1 )
assume A15: ( a => b = Top L1 & b => c = Top L1 ) ; :: thesis: a => c = Top L1
a => c = (Top L1) => (a => c) by A2
.= (Top L1) => ((Top L1) => (a => c)) by A2
.= (a => (Top L1)) => ((Top L1) => (a => c)) by A13
.= Top L1 by A2, A15 ;
hence a => c = Top L1 ; :: thesis: verum
end;
A16: L1 is satisfying_A1b
proof
let a, b, c be Element of L1; :: according to NELSON_1:def 8 :: thesis: ( a < b & b < c implies a < c )
assume ( a < b & b < c ) ; :: thesis: a < c
hence a < c by A14; :: thesis: verum
end;
A17: L1 is satisfying_N6
proof
let a, b, c be Element of L1; :: according to NELSON_1:def 13 :: thesis: ( a < c & b < c implies a "\/" b < c )
assume A18: ( a < c & b < c ) ; :: thesis: a "\/" b < c
(a => c) => ((b => c) => ((a "\/" b) => c)) = Top L1 by A2;
then (b => c) => ((a "\/" b) => c) = Top L1 by A18, A2;
hence a "\/" b < c by A2, A18; :: thesis: verum
end;
A19: for a being Element of L1 holds a => a = Top L1
proof
let a be Element of L1; :: thesis: a => a = Top L1
A20: (a => ((a => a) => a)) => ((a => (a => a)) => (a => a)) = Top L1 by A2;
a => ((a => a) => a) = Top L1 by A2;
then A21: (a => (a => a)) => (a => a) = Top L1 by A20, A2;
a => (a => a) = Top L1 by A2;
hence a => a = Top L1 by A21, A2; :: thesis: verum
end;
A22: L1 is satisfying_N7
proof
let a, b, c be Element of L1; :: according to NELSON_1:def 14 :: thesis: ( a < b & a < c implies a < b "/\" c )
assume A23: ( a < b & a < c ) ; :: thesis: a < b "/\" c
(a => b) => ((a => c) => (a => (b "/\" c))) = Top L1 by A2;
then (a => c) => (a => (b "/\" c)) = Top L1 by A23, A2;
hence a < b "/\" c by A2, A23; :: thesis: verum
end;
A24: for a, b being Element of L1 holds b < a "\/" b by A2;
A25: for a, b being Element of L1 holds a "/\" b <= a
proof
let a, b be Element of L1; :: thesis: a "/\" b <= a
A26: - (a "/\" b) = (- a) "\/" (- b) by A2;
A27: a "/\" b < a by A2;
- a < (- a) "\/" (- b) by A2;
hence a "/\" b <= a by A27, A6, A26; :: thesis: verum
end;
A28: for a, b being Element of L1 holds a <= a "\/" b
proof
let a, b be Element of L1; :: thesis: a <= a "\/" b
A29: (- a) "/\" (- b) < - a by A2;
A30: a < a "\/" b by A2;
- (a "\/" b) = (- a) "/\" (- b) by A2;
hence a <= a "\/" b by A29, A30, A6; :: thesis: verum
end;
A31: for a, b being Element of L1 holds b <= a "\/" b
proof
let a, b be Element of L1; :: thesis: b <= a "\/" b
A32: b < a "\/" b by A2;
A33: - (a "\/" b) = (- a) "/\" (- b) by A2;
(- a) "/\" (- b) < - b by A2;
hence b <= a "\/" b by A6, A32, A33; :: thesis: verum
end;
A34: for a, b being Element of L1 holds a "/\" b <= b
proof
let a, b be Element of L1; :: thesis: a "/\" b <= b
A35: - (a "/\" b) = (- a) "\/" (- b) by A2;
A36: a "/\" b < b by A2;
- b < (- a) "\/" (- b) by A2;
hence a "/\" b <= b by A35, A36, A6; :: thesis: verum
end;
A37: for a being Element of L1 holds a =-> a = Top L1
proof
let a be Element of L1; :: thesis: a =-> a = Top L1
a =-> a = (a => a) "/\" ((- a) => (- a)) by A2
.= (Top L1) "/\" ((- a) => (- a)) by A19
.= Top L1 by A19, A5 ;
hence a =-> a = Top L1 ; :: thesis: verum
end;
A38: for a, b being Element of L1 holds
( a = b iff ( a =-> b = Top L1 & b =-> a = Top L1 ) )
proof
let a, b be Element of L1; :: thesis: ( a = b iff ( a =-> b = Top L1 & b =-> a = Top L1 ) )
( a =-> b = Top L1 & b =-> a = Top L implies a = b )
proof
assume A39: ( a =-> b = Top L1 & b =-> a = Top L ) ; :: thesis: a = b
then (b =-> a) => ((a =-> b) => a) = (Top L1) => ((b =-> a) => b) by A2;
then (b =-> a) => ((a =-> b) => a) = (Top L1) => b by A2, A39;
then (b =-> a) => ((Top L1) => a) = b by A39, A2;
then (Top L1) => a = b by A39, A2;
hence a = b by A2; :: thesis: verum
end;
hence ( a = b iff ( a =-> b = Top L1 & b =-> a = Top L1 ) ) by A37; :: thesis: verum
end;
A40: for a, b being Element of L1 holds
( ( a <= b & b <= a ) iff a = b )
proof
let a, b be Element of L1; :: thesis: ( ( a <= b & b <= a ) iff a = b )
thus ( a <= b & b <= a implies a = b ) :: thesis: ( a = b implies ( a <= b & b <= a ) )
proof
assume ( a <= b & b <= a ) ; :: thesis: a = b
then ( a =-> b = Top L & b =-> a = Top L ) by A1;
hence a = b by A38; :: thesis: verum
end;
assume a = b ; :: thesis: ( a <= b & b <= a )
then ( a =-> b = Top L & b =-> a = Top L ) by A38;
hence ( a <= b & b <= a ) by A1; :: thesis: verum
end;
A41: for b being Element of L1 st Top L1 < b holds
b = Top L1 by A2;
A42: L1 is satisfying_A1
proof
let a be Element of L1; :: according to NELSON_1:def 7 :: thesis: a < a
thus a < a by A19; :: thesis: verum
end;
A43: for a, b, c being Element of L1 st a < b holds
( b => c < a => c & c => a < c => b )
proof
let a, b, c be Element of L1; :: thesis: ( a < b implies ( b => c < a => c & c => a < c => b ) )
assume A44: a < b ; :: thesis: ( b => c < a => c & c => a < c => b )
A45: b => c < a => (b => c) by A2;
a => (b => c) < (a => b) => (a => c) by A2;
then A46: b => c < (a => b) => (a => c) by A45, A16;
(c => (Top L1)) => ((c => a) => (c => b)) = Top L1 by A2, A44;
then (Top L1) => ((c => a) => (c => b)) = Top L1 by A13;
hence ( b => c < a => c & c => a < c => b ) by A46, A2, A44; :: thesis: verum
end;
A47: for a, b being Element of L1 holds a => (b => (a "/\" b)) = Top L1
proof
let a, b be Element of L1; :: thesis: a => (b => (a "/\" b)) = Top L1
b => a < (b => b) => (b => (a "/\" b)) by A2;
then b => a < (Top L1) => (b => (a "/\" b)) by A19;
then b => a < b => (a "/\" b) by A2;
then a => (b => a) < a => (b => (a "/\" b)) by A43;
then Top L1 < a => (b => (a "/\" b)) by A2;
hence a => (b => (a "/\" b)) = Top L1 by A2; :: thesis: verum
end;
A48: for a, b, c being Element of L1 st a < b => c holds
b < a => c
proof
let a, b, c be Element of L1; :: thesis: ( a < b => c implies b < a => c )
assume A49: a < b => c ; :: thesis: b < a => c
a => (b => c) < (a => b) => (a => c) by A2;
then A50: a => b < a => c by A2, A49;
b < a => b by A2;
hence b < a => c by A50, A16; :: thesis: verum
end;
A51: for a, c being Element of L1 holds a => (a => c) < a => c
proof
let a, c be Element of L1; :: thesis: a => (a => c) < a => c
a => (a => c) < (a => a) => (a => c) by A2;
then a => (a => c) < (Top L1) => (a => c) by A19;
hence a => (a => c) < a => c by A2; :: thesis: verum
end;
A52: L1 is satisfying_N3
proof
let x, a, b be Element of L1; :: according to NELSON_1:def 10 :: thesis: ( a "/\" x < b iff x < a => b )
A53: ( a "/\" x < b implies x < a => b )
proof
assume a "/\" x < b ; :: thesis: x < a => b
then x => (a "/\" x) < x => b by A43;
then A54: a => (x => (a "/\" x)) < a => (x => b) by A43;
a => (x => (a "/\" x)) = Top L1 by A47;
then a < x => b by A2, A54;
hence x < a => b by A48; :: thesis: verum
end;
( x < a => b implies a "/\" x < b )
proof
assume A55: x < a => b ; :: thesis: a "/\" x < b
a "/\" x < x by A2;
then a "/\" x < a => b by A55, A16;
then A56: a < (a "/\" x) => b by A48;
a "/\" x < a by A2;
then a "/\" x < (a "/\" x) => b by A16, A56;
hence a "/\" x < b by A41, A51; :: thesis: verum
end;
hence ( a "/\" x < b iff x < a => b ) by A53; :: thesis: verum
end;
A57: for a, b, c being Element of L1 st b < c holds
a "/\" b < a "/\" c
proof
let a, b, c be Element of L1; :: thesis: ( b < c implies a "/\" b < a "/\" c )
assume A58: b < c ; :: thesis: a "/\" b < a "/\" c
a "/\" b < b by A2;
then A59: a "/\" b < c by A58, A16;
a "/\" b < a by A2;
hence a "/\" b < a "/\" c by A22, A59; :: thesis: verum
end;
A58: for a, b, c being Element of L1 st b < c holds
a "\/" b < a "\/" c
proof
let a, b, c be Element of L1; :: thesis: ( b < c implies a "\/" b < a "\/" c )
assume A60: b < c ; :: thesis: a "\/" b < a "\/" c
A61: a < a "\/" c by A2;
c < a "\/" c by A2;
then b < a "\/" c by A60, A16;
hence a "\/" b < a "\/" c by A61, A17; :: thesis: verum
end;
A62: for a, b, c being Element of L1 st a <= c & b <= c holds
a "\/" b <= c
proof
let a, b, c be Element of L1; :: thesis: ( a <= c & b <= c implies a "\/" b <= c )
assume A63: ( a <= c & b <= c ) ; :: thesis: a "\/" b <= c
then A64: ( a < c & - c < - a ) by A6;
A65: ( b < c & - c < - b ) by A63, A6;
((- c) => (- a)) => (((- c) => (- b)) => ((- c) => ((- a) "/\" (- b)))) = Top L1 by A2;
then ((- c) => (- b)) => ((- c) => ((- a) "/\" (- b))) = Top L1 by A64, A2;
then (- c) => ((- a) "/\" (- b)) = Top L1 by A65, A2;
then - c < - (a "\/" b) by A2;
hence a "\/" b <= c by A65, A64, A17, A6; :: thesis: verum
end;
A66: for a, b, c being Element of L1 st c <= a & c <= b holds
c <= a "/\" b
proof
let a, b, c be Element of L1; :: thesis: ( c <= a & c <= b implies c <= a "/\" b )
assume A67: ( c <= a & c <= b ) ; :: thesis: c <= a "/\" b
then A68: ( c < a & - a < - c ) by A6;
A69: ( c < b & - b < - c ) by A67, A6;
((- a) => (- c)) => (((- b) => (- c)) => (((- a) "\/" (- b)) => (- c))) = Top L1 by A2;
then ((- b) => (- c)) => (((- a) "\/" (- b)) => (- c)) = Top L1 by A68, A2;
then ((- a) "\/" (- b)) => (- c) = Top L1 by A69, A2;
then - (a "/\" b) < - c by A2;
hence c <= a "/\" b by A69, A68, A22, A6; :: thesis: verum
end;
A70: for a, b being Element of L1 holds b "\/" a <= a "\/" b
proof
let a, b be Element of L1; :: thesis: b "\/" a <= a "\/" b
A71: a <= a "\/" b by A28;
b <= a "\/" b by A31;
hence b "\/" a <= a "\/" b by A71, A62; :: thesis: verum
end;
A72: for a, b being Element of L1 holds a "\/" b = b "\/" a
proof
let a, b be Element of L1; :: thesis: a "\/" b = b "\/" a
A73: a "\/" b <= b "\/" a by A70;
b "\/" a <= a "\/" b by A70;
hence a "\/" b = b "\/" a by A73, A40; :: thesis: verum
end;
A74: for a, b being Element of L1 holds a "/\" b <= b "/\" a
proof
let a, b be Element of L1; :: thesis: a "/\" b <= b "/\" a
A75: a "/\" b <= a by A25;
a "/\" b <= b by A34;
hence a "/\" b <= b "/\" a by A75, A66; :: thesis: verum
end;
for a, b being Element of L1 holds a "/\" b = b "/\" a
proof
let a, b be Element of L1; :: thesis: a "/\" b = b "/\" a
A76: a "/\" b <= b "/\" a by A74;
b "/\" a <= a "/\" b by A74;
hence a "/\" b = b "/\" a by A40, A76; :: thesis: verum
end;
then reconsider L1 = L1 as non empty join-commutative meet-commutative DeMorgan NelsonStr by A72, LATTICES:def 4, LATTICES:def 6;
A77: for a, b, c being Element of L1 st a <= b holds
a "\/" c <= b "\/" c
proof
let a, b, c be Element of L1; :: thesis: ( a <= b implies a "\/" c <= b "\/" c )
assume a <= b ; :: thesis: a "\/" c <= b "\/" c
then A78: ( a < b & - b < - a ) by A6;
then (- b) "/\" (- c) < (- a) "/\" (- c) by A57;
then - (b "\/" c) < (- a) "/\" (- c) by A2;
then - (b "\/" c) < - (a "\/" c) by A2;
hence a "\/" c <= b "\/" c by A78, A58, A6; :: thesis: verum
end;
set d = - (Top L1);
A79: for a being Element of L1 holds
( (- (Top L1)) "/\" a = - (Top L1) & a "/\" (- (Top L1)) = - (Top L1) ) by A12;
for a, b being Element of L1 holds b = (a "/\" b) "\/" b
proof
let a, b be Element of L1; :: thesis: b = (a "/\" b) "\/" b
A80: b <= (a "/\" b) "\/" b by A31;
( a "/\" b <= b & b <= b ) by A40, A25;
then (a "/\" b) "\/" b <= b by A62;
hence b = (a "/\" b) "\/" b by A80, A40; :: thesis: verum
end;
then A81: L1 is meet-absorbing ;
for a, b being Element of L1 holds a "/\" (a "\/" b) = a
proof
let a, b be Element of L1; :: thesis: a "/\" (a "\/" b) = a
( a <= a & a <= a "\/" b ) by A40, A31;
hence a "/\" (a "\/" b) = a ; :: thesis: verum
end;
then A82: L1 is join-absorbing ;
A83: for a, b, c being Element of L1 st b <= c holds
a "/\" b <= a "/\" c
proof
let a, b, c be Element of L1; :: thesis: ( b <= c implies a "/\" b <= a "/\" c )
assume A84: b <= c ; :: thesis: a "/\" b <= a "/\" c
then A85: a "/\" b < a "/\" c by A57, A6;
- (a "/\" c) < - (a "/\" b)
proof
- c < - b by A84, A6;
then (- a) "\/" (- c) < (- a) "\/" (- b) by A58;
then - (a "/\" c) < (- a) "\/" (- b) by A2;
hence - (a "/\" c) < - (a "/\" b) by A2; :: thesis: verum
end;
hence a "/\" b <= a "/\" c by A85, A6; :: thesis: verum
end;
A86: for a, b, c being Element of L1 st a <= b & b <= c holds
a <= c
proof
let a, b, c be Element of L1; :: thesis: ( a <= b & b <= c implies a <= c )
assume ( a <= b & b <= c ) ; :: thesis: a <= c
then ( a < b & b < c & - c < - b & - b < - a ) by A6;
then ( a < c & - c < - a ) by A14;
hence a <= c by A6; :: thesis: verum
end;
A87: for a, b, c being Element of L1 holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of L1; :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
A88: a "/\" (b "/\" c) <= a "/\" b by A34, A83;
A89: a "/\" (b "/\" c) <= b "/\" c by A34;
b "/\" c <= c by A34;
then a "/\" (b "/\" c) <= c by A86, A89;
then A90: a "/\" (b "/\" c) <= (a "/\" b) "/\" c by A88, A66;
A91: a "/\" b <= a by A25;
(a "/\" b) "/\" c <= a "/\" b by A25;
then A92: (a "/\" b) "/\" c <= a by A91, A86;
(a "/\" b) "/\" c <= b "/\" c by A25, A83;
then (a "/\" b) "/\" c <= a "/\" (b "/\" c) by A92, A66;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c by A90, A40; :: thesis: verum
end;
for a, b, c being Element of L1 holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of L1; :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
A93: a <= a "\/" b by A28;
a "\/" b <= (a "\/" b) "\/" c by A28;
then A94: a <= (a "\/" b) "\/" c by A86, A93;
b "\/" c <= (a "\/" b) "\/" c by A28, A77;
then A95: a "\/" (b "\/" c) <= (a "\/" b) "\/" c by A94, A62;
A96: c <= b "\/" c by A28;
b "\/" c <= a "\/" (b "\/" c) by A28;
then A97: c <= a "\/" (b "\/" c) by A96, A86;
a "\/" b <= a "\/" (b "\/" c) by A28, A77;
then (a "\/" b) "\/" c <= a "\/" (b "\/" c) by A97, A62;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c by A95, A40; :: thesis: verum
end;
then ( L1 is join-associative & L1 is meet-associative ) by A87;
then reconsider L1 = L1 as non empty Lattice-like lower-bounded DeMorgan NelsonStr by A81, A79, A82, LATTICES:def 13;
set c = Top L1;
for a being Element of L1 holds
( (Top L1) "\/" a = Top L1 & a "\/" (Top L1) = Top L1 )
proof
let a be Element of L1; :: thesis: ( (Top L1) "\/" a = Top L1 & a "\/" (Top L1) = Top L1 )
a <= Top L1 by A8;
hence ( (Top L1) "\/" a = Top L1 & a "\/" (Top L1) = Top L1 ) by LATTICES:4, LATTICES:def 3; :: thesis: verum
end;
then L is upper-bounded ;
then reconsider L1 = L1 as non empty Lattice-like bounded involutive DeMorgan NelsonStr by A2;
A98: L1 is distributive
proof
let a, b, c be Element of L1; :: according to LATTICES:def 11 :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
A99: b < a => ((a "/\" b) "\/" (a "/\" c)) by A52, A24;
c < a => ((a "/\" b) "\/" (a "/\" c)) by A52, A24;
then A100: b "\/" c < a => ((a "/\" b) "\/" (a "/\" c)) by A99, A17;
A101: for a, b, c being Element of L1 holds a "/\" (b "\/" c) < (a "/\" b) "\/" (a "/\" c)
proof
let a, b, c be Element of L1; :: thesis: a "/\" (b "\/" c) < (a "/\" b) "\/" (a "/\" c)
A102: b < a => ((a "/\" b) "\/" (a "/\" c)) by A52, A24;
c < a => ((a "/\" b) "\/" (a "/\" c)) by A52, A24;
then b "\/" c < a => ((a "/\" b) "\/" (a "/\" c)) by A102, A17;
hence a "/\" (b "\/" c) < (a "/\" b) "\/" (a "/\" c) by A52; :: thesis: verum
end;
A103: ((- a) "\/" (- b)) "/\" ((- a) "\/" (- c)) < (((- a) "\/" (- b)) "/\" (- a)) "\/" (((- a) "\/" (- b)) "/\" (- c)) by A101;
A104: (((- a) "\/" (- b)) "/\" (- a)) "\/" (((- a) "\/" (- b)) "/\" (- c)) = (- a) "\/" (((- a) "\/" (- b)) "/\" (- c)) by LATTICES:def 9;
(- a) "\/" ((- c) "/\" ((- a) "\/" (- b))) < (- a) "\/" (((- c) "/\" (- a)) "\/" ((- c) "/\" (- b))) by A101, A58;
then A105: ((- a) "\/" (- b)) "/\" ((- a) "\/" (- c)) < (- a) "\/" (((- a) "/\" (- c)) "\/" ((- b) "/\" (- c))) by A16, A103, A104;
(- a) "\/" (((- a) "/\" (- c)) "\/" ((- b) "/\" (- c))) = ((- a) "\/" ((- a) "/\" (- c))) "\/" ((- b) "/\" (- c)) by LATTICES:def 5
.= (- a) "\/" ((- b) "/\" (- c)) by LATTICES:def 8
.= (- a) "\/" (- (b "\/" c)) by A2 ;
then ((- a) "\/" (- b)) "/\" (- (a "/\" c)) < (- a) "\/" (- (b "\/" c)) by A2, A105;
then (- (a "/\" b)) "/\" (- (a "/\" c)) < (- a) "\/" (- (b "\/" c)) by A2;
then (- (a "/\" b)) "/\" (- (a "/\" c)) < - (a "/\" (b "\/" c)) by A2;
then - ((a "/\" b) "\/" (a "/\" c)) < - (a "/\" (b "\/" c)) by A2;
then A106: a "/\" (b "\/" c) <= (a "/\" b) "\/" (a "/\" c) by A6, A100, A52;
A107: a "/\" b <= a "/\" (b "\/" c) by A28, A83;
a "/\" c <= a "/\" (b "\/" c) by A28, A83;
then (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c) by A62, A107;
hence a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by A106, A40; :: thesis: verum
end;
reconsider L1 = L1 as non empty Lattice-like distributive bounded involutive DeMorgan NelsonStr by A98;
A108: L1 is satisfying_N5
proof
let a, b be Element of L1; :: according to NELSON_1:def 12 :: thesis: ( a =-> b = Top L1 iff a "/\" b = a )
A109: ( a =-> b = Top L1 implies a "/\" b = a )
proof
assume a =-> b = Top L1 ; :: thesis: a "/\" b = a
then a <= b by A1;
hence a "/\" b = a ; :: thesis: verum
end;
( a "/\" b = a implies a =-> b = Top L1 )
proof
assume a "/\" b = a ; :: thesis: a =-> b = Top L1
then a <= b ;
hence a =-> b = Top L1 by A1; :: thesis: verum
end;
hence ( a =-> b = Top L1 iff a "/\" b = a ) by A109; :: thesis: verum
end;
A110: L1 is satisfying_N8
proof
let a, b be Element of L1; :: according to NELSON_1:def 15 :: thesis: a "/\" (- b) < - (a => b)
((- (a => b)) => (a "/\" (- b))) "/\" ((a "/\" (- b)) => (- (a => b))) = Top L1 by A2;
hence a "/\" (- b) < - (a => b) by A3; :: thesis: verum
end;
A111: L1 is satisfying_N9
proof
let a, b be Element of L1; :: according to NELSON_1:def 16 :: thesis: - (a => b) < a "/\" (- b)
((- (a => b)) => (a "/\" (- b))) "/\" ((a "/\" (- b)) => (- (a => b))) = Top L1 by A2;
hence - (a => b) < a "/\" (- b) by A3; :: thesis: verum
end;
A112: L1 is satisfying_N10
proof
let a be Element of L1; :: according to NELSON_1:def 17 :: thesis: a < - (! a)
((- (! a)) => a) "/\" (a => (- (! a))) = Top L1 by A2;
hence a < - (! a) by A3; :: thesis: verum
end;
A113: L1 is satisfying_N11
proof
let a be Element of L1; :: according to NELSON_1:def 18 :: thesis: - (! a) < a
((- (! a)) => a) "/\" (a => (- (! a))) = Top L1 by A2;
hence - (! a) < a by A3; :: thesis: verum
end;
A114: L1 is satisfying_N12
proof
let a, b be Element of L1; :: according to NELSON_1:def 19 :: thesis: a "/\" (- a) < b
- a < a => b by A2;
hence a "/\" (- a) < b by A52; :: thesis: verum
end;
A115: for a, b, c being Element of L1 holds ! (Top L1) = - (Top L1)
proof
let a, b, c be Element of L1; :: thesis: ! (Top L1) = - (Top L1)
A116: - (Top L1) <= ! (Top L1) by A10;
! (Top L1) <= - (Top L1)
proof
(! (a => a)) => (- (Top L1)) = Top L1 by A2;
then A117: ! (Top L1) < - (Top L1) by A19;
A118: - (- (Top L1)) = Top L1 by A2;
Top L1 < - (! (Top L1)) by A112;
hence ! (Top L1) <= - (Top L1) by A117, A118, A6; :: thesis: verum
end;
hence ! (Top L1) = - (Top L1) by A116, A40; :: thesis: verum
end;
A119: for a, b being Element of L1 holds a => (! b) = b => (! a)
proof
let a, b be Element of L1; :: thesis: a => (! b) = b => (! a)
A120: a => (! b) < b => (! a) by A2;
A121: - (b => (! a)) < b "/\" (- (! a)) by A111;
b "/\" (- (! a)) < b "/\" a by A113, A57;
then A122: - (b => (! a)) < a "/\" b by A121, A16;
A123: a "/\" b < a "/\" (- (! b)) by A112, A57;
a "/\" (- (! b)) < - (a => (! b)) by A110;
then a "/\" b < - (a => (! b)) by A123, A16;
then - (b => (! a)) < - (a => (! b)) by A16, A122;
then A124: a => (! b) <= b => (! a) by A120, A6;
A125: b => (! a) < a => (! b) by A2;
A126: - (a => (! b)) < a "/\" (- (! b)) by A111;
a "/\" (- (! b)) < a "/\" b by A113, A57;
then A127: - (a => (! b)) < b "/\" a by A126, A16;
A128: b "/\" a < b "/\" (- (! a)) by A112, A57;
b "/\" (- (! a)) < - (b => (! a)) by A110;
then b "/\" a < - (b => (! a)) by A128, A16;
then - (a => (! b)) < - (b => (! a)) by A16, A127;
then b => (! a) <= a => (! b) by A125, A6;
hence a => (! b) = b => (! a) by A124, A40; :: thesis: verum
end;
L1 is satisfying_N13
proof
let a be Element of L1; :: according to NELSON_1:def 20 :: thesis: ! a = a => (- (Top L1))
! a = (Top L1) => (! a) by A2
.= a => (! (Top L1)) by A119
.= a => (- (Top L1)) by A115 ;
hence ! a = a => (- (Top L1)) ; :: thesis: verum
end;
hence L is Nelson_Algebra by A108, A42, A52, A2, A17, A22, A110, A111, A112, A113, A114, A16; :: thesis: verum