set L = QLTLattice1 ;
for v0, v2, v1 being Element of QLTLattice1 holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
proof
let v0, v2, v1 be Element of QLTLattice1; :: thesis: (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
reconsider z = 0 as Element of QLTLattice1 by ENUMSET1:def 1;
per cases ( ( v0 = v1 & v1 = v2 ) or ( v0 = v1 & v1 <> v2 ) or ( v0 <> v1 & v1 <> v2 ) or ( v0 <> v1 & v1 = v2 ) ) ;
suppose ( v0 = v1 & v1 = v2 ) ; :: thesis: (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
then ( v1 "\/" v2 = v1 & v0 "/\" v1 = v0 ) by QLTEx1Def;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by ROBBINS1:def 7; :: thesis: verum
end;
suppose ( v0 = v1 & v1 <> v2 ) ; :: thesis: (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
then A1: ( v1 "\/" v2 = 0 & v0 "/\" v1 = v0 ) by QLTEx1Def;
then (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = z "\/" v0 by Lemacik00
.= z by Lemacik001
.= v0 "/\" (v1 "\/" v2) by A1, Lemacik00 ;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ; :: thesis: verum
end;
suppose ( v0 <> v1 & v1 <> v2 ) ; :: thesis: (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
then A1: ( v1 "\/" v2 = 0 & v0 "/\" v1 = 0 ) by QLTEx1Def;
then (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = z by Lemacik001
.= v0 "/\" (v1 "\/" v2) by A1, Lemacik00 ;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ; :: thesis: verum
end;
suppose ( v0 <> v1 & v1 = v2 ) ; :: thesis: (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)
then ( v1 "\/" v2 = v1 & v0 "/\" v1 = 0 ) by QLTEx1Def;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by Lemacik001; :: thesis: verum
end;
end;
end;
hence QLTLattice1 is satisfying_QLT1 ; :: thesis: verum