let v0, v1 be Element of QLTLattice1; :: thesis: ( v1 = 0 implies v0 "/\" v1 = v1 )
assume A1: v1 = 0 ; :: thesis: v0 "/\" v1 = v1
per cases ( v0 = v1 or v0 <> v1 ) ;
suppose v0 = v1 ; :: thesis: v0 "/\" v1 = v1
hence v0 "/\" v1 = v1 by QLTEx1Def; :: thesis: verum
end;
suppose v0 <> v1 ; :: thesis: v0 "/\" v1 = v1
hence v0 "/\" v1 = v1 by A1, QLTEx1Def; :: thesis: verum
end;
end;