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;