set L = ExNearLattice ;
for v2, v1, v0 being Element of ExNearLattice holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1
proof
let v2,
v1,
v0 be
Element of
ExNearLattice;
((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1
a1:
v2 in {0,1,2}
by LATWAL_1:def 10;
then A1:
(
v2 = 2 or
v2 = 1 or
v2 = 0 )
by ENUMSET1:def 1;
a2:
v1 in {0,1,2}
by LATWAL_1:def 10;
then A2:
(
v1 = 2 or
v1 = 1 or
v1 = 0 )
by ENUMSET1:def 1;
a3:
v0 in {0,1,2}
by LATWAL_1:def 10;
then A3:
(
v0 = 2 or
v0 = 1 or
v0 = 0 )
by ENUMSET1:def 1;
reconsider a =
v0,
b =
v1,
c =
v2 as
Element of
{0,1,2} by a1, a2, a3;
per cases
( ( v2 = 2 & v1 = 2 & v0 = 2 ) or ( v2 = 2 & v1 = 2 & v0 = 1 ) or ( v2 = 2 & v1 = 2 & v0 = 0 ) or ( v2 = 1 & v1 = 1 & v0 = 1 ) or ( v2 = 0 & v1 = 0 & v0 = 0 ) or ( v2 = 2 & v1 = 0 & v0 = 2 ) or ( v2 = 0 & v1 = 2 & v0 = 2 ) or ( v2 = 2 & v1 = 1 & v0 = 1 ) or ( v2 = 0 & v1 = 0 & v0 = 1 ) or ( v2 = 0 & v1 = 0 & v0 = 2 ) or ( v2 = 0 & v1 = 0 & v0 = 1 ) or ( v2 = 0 & v1 = 1 & v0 = 0 ) or ( v2 = 0 & v1 = 1 & v0 = 1 ) or ( v2 = 0 & v1 = 1 & v0 = 2 ) or ( v2 = 0 & v1 = 2 & v0 = 0 ) or ( v2 = 0 & v1 = 2 & v0 = 1 ) or ( v2 = 1 & v1 = 0 & v0 = 0 ) or ( v2 = 1 & v1 = 0 & v0 = 1 ) or ( v2 = 1 & v1 = 0 & v0 = 2 ) or ( v2 = 1 & v1 = 1 & v0 = 0 ) or ( v2 = 1 & v1 = 1 & v0 = 2 ) or ( v2 = 1 & v1 = 2 & v0 = 0 ) or ( v2 = 1 & v1 = 2 & v0 = 1 ) or ( v2 = 1 & v1 = 2 & v0 = 2 ) or ( v2 = 1 & v1 = 2 & v0 = 2 ) or ( v2 = 2 & v1 = 0 & v0 = 0 ) or ( v2 = 2 & v1 = 0 & v0 = 1 ) or ( v2 = 2 & v1 = 1 & v0 = 0 ) or ( v2 = 2 & v1 = 1 & v0 = 2 ) )
by A1, A2, A3;
end;
end;
hence
ExNearLattice is satisfying_W3'
by LATWAL_1:def 2; verum