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: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)
reconsider z = 0 as Element of QLTLattice2 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 ) ) by ENUMSET1:def 1;

suppose ( v0 = v1 & v1 = v2 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then ( v1 "/\" v2 = v1 & v0 "\/" v1 = v1 ) by BINOP_1:def 4;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by SHEFFER1:def 9; :: thesis: verum

end;

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

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

end;

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

per cases ( v2 = 1 or v2 <> 1 ) ;

suppose v2 = 1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then A1: ( v1 "/\" v2 = 1 & v0 "\/" v1 = v0 ) by QLTEx1Def, QLTEx2Def, A0;
P4: v0 "/\" z = min (v0,z) by A0, QLTEx2Def
.= z by A0 ;
(v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = z by P4, QLTEx1Def, A0, A1;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by QLTEx1Def, A0, A1; :: thesis: verum

end;

suppose v2 <> 1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then A1: ( v1 "/\" v2 = min (v1,v2) & v0 "\/" v1 = v0 ) by QLTEx1Def, QLTEx2Def, A0;
P3: v1 <= v2 by A0, ENUMSET1:def 1;
v1 "/\" v2 = v1 by XXREAL_0:def 9, P3, A1;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by SHEFFER1:def 9; :: thesis: verum

end;

end;

end;

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

P4: v0 "/\" z = min (v0,z) by A0, QLTEx2Def
.= z by XXREAL_0:def 9, A0 ;

per cases ( v2 = 1 or v2 <> 1 ) ;

suppose v2 = 1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

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

end;

suppose B: v2 <> 1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

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

per cases ( v2 = 0 or v2 = 2 ) by ENUMSET1:def 1, B;

suppose v2 = 0 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

(v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = z by QLTEx1Def, A0, A1, p4, P4;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by QLTEx1Def, A0, P4A; :: thesis: verum

end;

suppose v2 = 2 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by A0; :: thesis: verum

end;

end;

end;

end;

end;

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

per cases ( v2 = 1 or v2 <> 1 ) ;

suppose v2 = 1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

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

end;

suppose B: v2 <> 1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

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

per cases ( min (v1,v2) = v1 or min (v1,v2) = v2 ) by XXREAL_0:15;

suppose C1: min (v1,v2) = v1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

(v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = (v0 "\/" v1) "/\" (v0 "\/" v1) by B, C1, QLTEx2Def, A0
.= v0 "\/" v1 by SHEFFER1:def 9 ;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by B, C1, QLTEx2Def, A0; :: thesis: verum

end;

suppose D1: min (v1,v2) = v2 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = z "/\" z by A0, B, QLTEx1Def, A1
.= z by BINOP_1:def 4 ;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by A0, B, QLTEx1Def, A1, D1; :: thesis: verum

end;

end;

end;

end;

end;

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

per cases ( v2 = 1 or v1 = 1 or ( v2 <> 1 & v1 <> 1 ) ) ;

suppose ( v2 = 1 or v1 = 1 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

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

end;

suppose B: ( v2 <> 1 & v1 <> 1 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

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

per cases ( min (v1,v2) = v1 or min (v1,v2) = v2 ) by XXREAL_0:15;

suppose min (v1,v2) = v1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by SHEFFER1:def 9, A1; :: thesis: verum

end;

suppose D1: min (v1,v2) = v2 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

( ( v1 = 1 & v2 <> 1 ) or ( v1 = 0 & v2 <> 0 ) ) by A0, ENUMSET1:def 1;
then ( ( v1 = 1 & ( v2 = 0 or v2 = 2 ) ) or ( v1 = 0 & ( v2 = 1 or v2 = 2 ) ) ) by ENUMSET1:def 1;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by XXREAL_0:def 9, D1, B; :: thesis: verum

end;

end;

end;

end;

end;

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

per cases ( v2 = 1 or v1 = 1 or ( v2 <> 1 & v1 <> 1 ) ) ;

suppose ( v2 = 1 or v1 = 1 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

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

end;

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

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

per cases ( min (v1,v2) = v1 or min (v1,v2) = v2 ) by XXREAL_0:15;

suppose min (v1,v2) = v1 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by SHEFFER1:def 9, A1; :: thesis: verum

end;

suppose D1: min (v1,v2) = v2 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

per cases ( v2 = v0 or v2 <> v0 ) ;

suppose D2: v2 = v0 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

v0 "/\" z = min (v0,z) by QLTEx2Def, A0
.= v0 by A0 ;
then (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 by A1, D2, D1, QLTEx1Def;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by D2, QLTEx1Def, A1, D1; :: thesis: verum

end;

suppose D2: v2 <> v0 ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = z "/\" z by QLTEx1Def, A1, D1
.= z by BINOP_1:def 4 ;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by D2, QLTEx1Def, A1, D1; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose ( v0 <> v1 & v1 = v2 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then ( v1 "/\" v2 = v1 & v0 "\/" v1 = 0 ) by QLTEx1Def, BINOP_1:def 4;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by SHEFFER1:def 9; :: thesis: verum

end;

end;

end;

hence QLTLattice2 is satisfying_QLT2 ; :: thesis: verum