set L = ExWALattice ;
for v2, v1, v0 being Element of ExWALattice holds ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1
proof
set W =
{0,1,2,3,4};
let v2,
v1,
v0 be
Element of
ExWALattice;
((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1
reconsider a =
v0,
b =
v1,
c =
v2 as
Element of
{0,1,2,3,4} ;
per cases
( v1 = 0 or v1 = 4 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 = 1 & v0 = 3 ) or ( v2 = 0 & v1 = 1 & v0 = 4 ) or ( v2 = 0 & v1 = 2 & v0 = 0 ) or ( v2 = 0 & v1 = 2 & v0 = 1 ) or ( v2 = 0 & v1 = 2 & v0 = 2 ) or ( v2 = 0 & v1 = 2 & v0 = 3 ) or ( v2 = 0 & v1 = 2 & v0 = 4 ) or ( v2 = 0 & v1 = 3 & v0 = 0 ) or ( v2 = 0 & v1 = 3 & v0 = 1 ) or ( v2 = 0 & v1 = 3 & v0 = 2 ) or ( v2 = 0 & v1 = 3 & v0 = 3 ) or ( v2 = 0 & v1 = 3 & v0 = 4 ) or ( v2 = 1 & v1 = 1 & v0 = 0 ) or ( v2 = 1 & v1 = 1 & v0 = 1 ) or ( v2 = 1 & v1 = 1 & v0 = 2 ) or ( v2 = 1 & v1 = 1 & v0 = 3 ) or ( v2 = 1 & v1 = 1 & v0 = 4 ) 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 = 3 ) or ( v2 = 1 & v1 = 2 & v0 = 4 ) or ( v2 = 1 & v1 = 3 & v0 = 0 ) or ( v2 = 1 & v1 = 3 & v0 = 1 ) or ( v2 = 1 & v1 = 3 & v0 = 2 ) or ( v2 = 1 & v1 = 3 & v0 = 3 ) or ( v2 = 1 & v1 = 3 & v0 = 4 ) or ( v2 = 1 & v1 = 4 & v0 = 0 ) or ( v2 = 1 & v1 = 4 & v0 = 1 ) or ( v2 = 1 & v1 = 4 & v0 = 2 ) or ( v2 = 1 & v1 = 4 & v0 = 3 ) or ( v2 = 1 & v1 = 4 & v0 = 4 ) or ( v2 = 2 & v1 = 1 & v0 = 0 ) or ( v2 = 2 & v1 = 1 & v0 = 1 ) or ( v2 = 2 & v1 = 1 & v0 = 2 ) or ( v2 = 2 & v1 = 1 & v0 = 3 ) or ( v2 = 2 & v1 = 1 & v0 = 4 ) or ( v2 = 2 & v1 = 2 & v0 = 0 ) or ( v2 = 2 & v1 = 2 & v0 = 1 ) or ( v2 = 2 & v1 = 2 & v0 = 2 ) or ( v2 = 2 & v1 = 2 & v0 = 3 ) or ( v2 = 2 & v1 = 2 & v0 = 4 ) or ( v2 = 2 & v1 = 3 & v0 = 0 ) or ( v2 = 2 & v1 = 3 & v0 = 1 ) or ( v2 = 2 & v1 = 3 & v0 = 2 ) or ( v2 = 2 & v1 = 3 & v0 = 3 ) or ( v2 = 2 & v1 = 3 & v0 = 4 ) or ( v2 = 2 & v1 = 4 & v0 = 0 ) or ( v2 = 2 & v1 = 4 & v0 = 1 ) or ( v2 = 2 & v1 = 4 & v0 = 2 ) or ( v2 = 2 & v1 = 4 & v0 = 3 ) or ( v2 = 2 & v1 = 4 & v0 = 4 ) or ( v2 = 3 & v1 = 1 & v0 = 0 ) or ( v2 = 3 & v1 = 1 & v0 = 1 ) or ( v2 = 3 & v1 = 1 & v0 = 2 ) or ( v2 = 3 & v1 = 1 & v0 = 3 ) or ( v2 = 3 & v1 = 1 & v0 = 4 ) or ( v2 = 3 & v1 = 2 & v0 = 0 ) or ( v2 = 3 & v1 = 2 & v0 = 1 ) or ( v2 = 3 & v1 = 2 & v0 = 2 ) or ( v2 = 3 & v1 = 2 & v0 = 3 ) or ( v2 = 3 & v1 = 2 & v0 = 4 ) or ( v2 = 3 & v1 = 3 & v0 = 0 ) or ( v2 = 3 & v1 = 3 & v0 = 1 ) or ( v2 = 3 & v1 = 3 & v0 = 2 ) or ( v2 = 3 & v1 = 3 & v0 = 3 ) or ( v2 = 3 & v1 = 3 & v0 = 4 ) or ( v2 = 3 & v1 = 4 & v0 = 0 ) or ( v2 = 3 & v1 = 4 & v0 = 1 ) or ( v2 = 3 & v1 = 4 & v0 = 2 ) or ( v2 = 3 & v1 = 4 & v0 = 3 ) or ( v2 = 3 & v1 = 4 & v0 = 4 ) or ( v2 = 4 & v1 = 1 & v0 = 0 ) or ( v2 = 4 & v1 = 1 & v0 = 1 ) or ( v2 = 4 & v1 = 1 & v0 = 2 ) or ( v2 = 4 & v1 = 1 & v0 = 3 ) or ( v2 = 4 & v1 = 1 & v0 = 4 ) or ( v2 = 4 & v1 = 2 & v0 = 0 ) or ( v2 = 4 & v1 = 2 & v0 = 1 ) or ( v2 = 4 & v1 = 2 & v0 = 2 ) or ( v2 = 4 & v1 = 2 & v0 = 3 ) or ( v2 = 4 & v1 = 2 & v0 = 4 ) or ( v2 = 4 & v1 = 3 & v0 = 0 ) or ( v2 = 4 & v1 = 3 & v0 = 1 ) or ( v2 = 4 & v1 = 3 & v0 = 2 ) or ( v2 = 4 & v1 = 3 & v0 = 3 ) or ( v2 = 4 & v1 = 3 & v0 = 4 ) or ( v2 = 4 & v1 = 4 & v0 = 0 ) or ( v2 = 4 & v1 = 4 & v0 = 1 ) or ( v2 = 4 & v1 = 4 & v0 = 2 ) or ( v2 = 4 & v1 = 4 & v0 = 3 ) or ( v2 = 4 & v1 = 4 & v0 = 4 ) )
by ENUMSET1:def 3;
end;
end;
hence
ExWALattice is satisfying_W3
by LATWAL_1:def 1; verum