set L = the non empty trivial NelsonStr ;
reconsider LL = the non empty trivial NelsonStr as non empty Lattice-like bounded NelsonStr ;
A1: LL is satisfying_A1

proof

let a be Element of LL; :: according to NELSON_1:def 7 :: thesis:
thus a < a by STRUCT_0:def 10; :: thesis:

end;

A2: LL is satisfying_A1b by STRUCT_0:def 10;
A3: LL is satisfying_N8

proof

let a, b be Element of LL; :: according to NELSON_1:def 15 :: thesis:
thus a "/\" (- b) < - (a => b) by STRUCT_0:def 10; :: thesis:

end;

A4: LL is satisfying_N9

proof

let a, b be Element of LL; :: according to NELSON_1:def 16 :: thesis:
thus - (a => b) < a "/\" (- b) by STRUCT_0:def 10; :: thesis:

end;

A5: ( LL is satisfying_A2 & LL is satisfying_N4 & LL is satisfying_N6 & LL is satisfying_N7 & LL is satisfying_N5 ) by STRUCT_0:def 10;
A6: LL is satisfying_N10

proof

let a be Element of LL; :: according to NELSON_1:def 17 :: thesis:
thus a < - (! a) by STRUCT_0:def 10; :: thesis:

end;

A7: LL is satisfying_N11

proof

let a be Element of LL; :: according to NELSON_1:def 18 :: thesis:
thus - (! a) < a by STRUCT_0:def 10; :: thesis:

end;

A8: LL is satisfying_N12

proof

let a be Element of LL; :: according to NELSON_1:def 19 :: thesis:
thus for b being Element of LL holds a "/\" (- a) < b by STRUCT_0:def 10; :: thesis:

end;

A9: LL is satisfying_N3

proof

let x, a, b be Element of LL; :: according to NELSON_1:def 10 :: thesis:
thus ( a "/\" x < b iff x < a => b ) by STRUCT_0:def 10; :: thesis:

end;

LL is satisfying_N13 by STRUCT_0:def 10;
hence ex b₁ being non empty Lattice-like bounded NelsonStr st
( b₁ is satisfying_A1 & b₁ is satisfying_A1b & b₁ is satisfying_A2 & b₁ is satisfying_N3 & b₁ is satisfying_N4 & b₁ is satisfying_N5 & b₁ is satisfying_N6 & b₁ is satisfying_N7 & b₁ is satisfying_N8 & b₁ is satisfying_N9 & b₁ is satisfying_N10 & b₁ is satisfying_N11 & b₁ is satisfying_N12 & b₁ is satisfying_N13 ) by A1, A2, A3, A4, A5, A6, A7, A8, A9; :: thesis: