set L = QLTLattice2 ;
for v0, v2, v1 being Element of QLTLattice2 holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
proof
let v0,
v2,
v1 be
Element of
QLTLattice2;
(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
reconsider z =
0 as
Element of
QLTLattice2 by ENUMSET1:def 1;
p2:
z <= v0
by ENUMSET1:def 1;
reconsider o = 1 as
Element of
QLTLattice2 by ENUMSET1:def 1;
reconsider dwa = 2 as
Element of
QLTLattice2 by ENUMSET1:def 1;
per cases
( ( v0 = v1 & v1 = v2 ) or ( v0 = v1 & v1 <> v2 & v0 = 1 ) or ( v0 = v1 & v1 <> v2 & v0 = 0 ) or ( v0 = v1 & v1 <> v2 & v0 = 2 ) or ( v0 <> v1 & v1 <> v2 & v0 = 1 ) or ( v0 <> v1 & v1 <> v2 & v0 = 2 ) or ( v0 <> v1 & v1 <> v2 & v0 = 0 ) or ( v0 <> v1 & v1 = v2 & v0 = 1 ) or ( v0 <> v1 & v1 = v2 & v0 = 0 ) or ( v0 <> v1 & v1 = v2 & v0 = 2 ) )
by ENUMSET1:def 1;
suppose A0:
(
v0 <> v1 &
v1 <> v2 &
v0 = 0 )
;
(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)per cases
( v1 = 1 or v1 <> 1 )
;
suppose
v1 <> 1
;
(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)then A1:
(
v1 "\/" v2 = 0 &
v0 "/\" v1 = min (
v0,
v1) )
by QLTEx1Def, QLTEx2Def, A0;
p2:
v0 <= v1
by A0, ENUMSET1:def 1;
P4:
v0 "/\" z =
min (
v0,
z)
by A0, QLTEx2Def
.=
z
by A0
;
(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) =
(v0 "/\" z) "\/" v0
by p2, A1, XXREAL_0:def 9
.=
v0 "/\" (v1 "\/" v2)
by A1, P4, QLTEx1Def, A0
;
hence
(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
;
verum end; end; end; end;
end;
hence
QLTLattice2 is satisfying_QLT1
; verum