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; :: thesis:
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 by ENUMSET1:def 1;

suppose ( v0 = v1 & v1 = v2 ) ; :: thesis:

then ( v1 "\/" v2 = v1 & v0 "/\" v1 = v1 ) by BINOP_1:def 4;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by ROBBINS1:def 7; :: thesis:

end;

suppose Z1: ( v0 = v1 & v1 <> v2 & v0 = 1 ) ; :: thesis:

then ( v1 "\/" v2 = 0 & v0 "/\" v1 = 1 ) by QLTEx1Def, BINOP_1:def 4;
then (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = o "\/" v0 by QLTEx2Def, Z1
.= o by QLTEx1Def, Z1
.= v0 "/\" (v1 "\/" v2) by Z1, QLTEx2Def ;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ; :: thesis:

end;

suppose A0: ( v0 = v1 & v1 <> v2 & v0 = 0 ) ; :: thesis:

then ( v1 "\/" v2 = 0 & v0 "/\" v1 = min (v0,v1) ) by QLTEx1Def, QLTEx2Def;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by QLTEx1Def, A0; :: thesis:

end;

suppose A0: ( v0 = v1 & v1 <> v2 & v0 = 2 ) ; :: thesis:

then A1: ( v1 "\/" v2 = 0 & v0 "/\" v1 = min (v0,v1) & v0 <> 1 ) by QLTEx1Def, QLTEx2Def;
v0 "/\" z = min (v0,z) by A0, QLTEx2Def
.= z by XXREAL_0:def 9, p2 ;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by A1, QLTEx1Def, A0; :: thesis:

end;

suppose A0: ( v0 <> v1 & v1 <> v2 & v0 = 1 ) ; :: thesis:

then A1: ( v1 "\/" v2 = 0 & v0 "/\" v1 = 1 ) by QLTEx1Def, QLTEx2Def;
v0 "/\" z = o by A0, QLTEx2Def;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by QLTEx1Def, A1; :: thesis:

end;

suppose A0: ( v0 <> v1 & v1 <> v2 & v0 = 2 ) ; :: thesis:

per cases ;

suppose v1 = 1 ; :: thesis:

then A1: ( v1 "\/" v2 = 0 & v0 "/\" v1 = 1 ) by QLTEx1Def, QLTEx2Def, A0;
v0 "/\" z = min (v0,z) by A0, QLTEx2Def
.= z by XXREAL_0:def 9, p2 ;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by QLTEx1Def, A1; :: thesis:

end;

suppose B: v1 <> 1 ; :: thesis:

then A1: ( v1 "\/" v2 = 0 & v0 "/\" v1 = min (v0,v1) ) by QLTEx1Def, QLTEx2Def, A0;
( v1 = 0 or v1 = 2 ) by ENUMSET1:def 1, B;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by QLTEx1Def, A0, A1; :: thesis:

end;

end;

end;

suppose A0: ( v0 <> v1 & v1 <> v2 & v0 = 0 ) ; :: thesis:

per cases ;

suppose v1 = 1 ; :: thesis:

then A1: ( v1 "\/" v2 = 0 & v0 "/\" v1 = 1 ) by QLTEx1Def, QLTEx2Def, A0;
v0 "/\" z = min (v0,z) by A0, QLTEx2Def
.= z by XXREAL_0:def 9, p2 ;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by A1, QLTEx1Def; :: thesis:

end;

suppose v1 <> 1 ; :: thesis:

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) ; :: thesis:

end;

end;

end;

suppose ( v0 <> v1 & v1 = v2 & v0 = 1 ) ; :: thesis:

then ( v1 "\/" v2 = v1 & v0 "/\" v1 = 1 ) by QLTEx1Def, QLTEx2Def;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by QLTEx1Def; :: thesis:

end;

suppose A0: ( v0 <> v1 & v1 = v2 & v0 = 0 ) ; :: thesis:

per cases ;

suppose v1 = 1 ; :: thesis:

then ( v1 "\/" v2 = v1 & v0 "/\" v1 = 1 ) by QLTEx1Def, QLTEx2Def, A0;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by ROBBINS1:def 7; :: thesis:

end;

suppose v1 <> 1 ; :: thesis:

then ( v1 "\/" v2 = v1 & v0 "/\" v1 = min (v0,v1) ) by QLTEx1Def, QLTEx2Def, A0;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by ROBBINS1:def 7; :: thesis:

end;

end;

end;

suppose A0: ( v0 <> v1 & v1 = v2 & v0 = 2 ) ; :: thesis:

per cases ;

suppose v1 = 1 ; :: thesis:

then ( v1 "\/" v2 = v1 & v0 "/\" v1 = 1 ) by QLTEx1Def, QLTEx2Def, A0;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by ROBBINS1:def 7; :: thesis:

end;

suppose v1 <> 1 ; :: thesis:

then ( v1 "\/" v2 = v1 & v0 "/\" v1 = min (v0,v1) ) by QLTEx1Def, QLTEx2Def, A0;
hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by ROBBINS1:def 7; :: thesis:

end;

end;

end;

end;

end;

hence QLTLattice2 is satisfying_QLT1 ; :: thesis: